From a9aa47b75a0ecdb7a18233797bb379e3a7bc14d0 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 8 Jan 2024 13:36:27 +0100 Subject: [PATCH] Redefine \min and \max in function_scope --- classical/mathcomp_extra.v | 6 ------ 1 file changed, 6 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index dbf90a224..59c5481c8 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,10 +1,6 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) Require Import BinPos. From mathcomp Require choice. -(* Missing coercion (done before Import to avoid redeclaration error, - thanks to KS for the trick) *) -(* MathComp 1.15 addition *) - From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From mathcomp Require Import finset interval. @@ -14,8 +10,6 @@ From mathcomp Require Import finset interval. (* This files contains lemmas and definitions missing from MathComp. *) (* *) (* ``` *) -(* f \max g := fun x => Num.max (f x) (g x) *) -(* f \min g := fun x => Num.min (f x) (g x) *) (* oflit f := Some \o f *) (* pred_oapp T D := [pred x | oapp (mem D) false x] *) (* f \* g := fun x => f x * g x *)