MathComp 2.3 compat

hivert · Jan 3, 2025 · 42be2a3 · 42be2a3
1 parent 7d804b9
commit 42be2a3
Show file tree

Hide file tree

Showing 10 changed files with 193 additions and 241 deletions.
diff --git a/Makefile b/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.19.2
+## GNUMakefile for Coq 8.20.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.19.2
+COQMAKEFILE_VERSION:=8.20.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -309,7 +309,7 @@ endif
 
 ifneq (,$(PROFILING))
   PROFILE_ARG=-profile $<.prof.json
-  PROFILE_ZIP=gzip $<.prof.json
+  PROFILE_ZIP=gzip -f $<.prof.json
 else
   PROFILE_ARG=
   PROFILE_ZIP=true
@@ -503,37 +503,6 @@ bytefiles: $(CMOFILES) $(CMAFILES)
 optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
-# FIXME, see Ralf's bugreport
-# quick is deprecated, now renamed vio
-vio: $(VOFILES:.vo=.vio)
-.PHONY: vio
-quick: vio
-	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
-.PHONY: quick
-
-vio2vo:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: vio2vo
-
-# quick2vo is undocumented
-quick2vo:
-	$(HIDE)make -j $(J) vio
-	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
-	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
-	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
-	done); \
-	echo "VIO2VO: $$VIOFILES"; \
-	if [ -n "$$VIOFILES" ]; then \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
-	fi
-.PHONY: quick2vo
-
-checkproofs:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: checkproofs
-
 vos: $(VOFILES:%.vo=%.vos)
 .PHONY: vos
 
@@ -711,9 +680,10 @@ clean::
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
 	$(HIDE)rm -f $(VOFILES)
-	$(HIDE)rm -f $(VOFILES:.vo=.vio)
 	$(HIDE)rm -f $(VOFILES:.vo=.vos)
 	$(HIDE)rm -f $(VOFILES:.vo=.vok)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json.gz)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -846,10 +816,6 @@ endif
 
 $(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile))))
 
-$(VFILES:.v=.vio): %.vio: %.v
-	$(SHOW)COQC -vio $<
-	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
 $(VFILES:.v=.vos): %.vos: %.v
 	$(SHOW)COQC -vos $<
 	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<

diff --git a/_CoqProject b/_CoqProject
@@ -4,6 +4,7 @@
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -deprecated-since-8.19
 -arg -w -arg -projection-no-head-constant
+-arg -w -arg -notation-incompatible-prefix
 theories/fps/directed.v
 theories/fps/invlim.v
 theories/fps/dirlim.v

diff --git a/theories/fps/directed.v b/theories/fps/directed.v
@@ -39,7 +39,7 @@ Definition directed (T : Type) (R : T -> T -> bool) :=
   forall x y : T, { z | R x z & R y z }.
 
 (** TODO : I'm not using anti-symmetry, i.e.: directed sets can be preorders *)
-HB.mixin Record Directed (d : unit) T of Order.POrder d T := {
+HB.mixin Record Directed d T of Order.POrder d T := {
   directedP : directed (T := T) <=%O
 }.
 #[short(type="dirType")]

diff --git a/theories/fps/dirlim.v b/theories/fps/dirlim.v
@@ -41,9 +41,8 @@ Unset Printing Implicit Defensive.
 
 #[key="dlT"]
 HB.factory Record isDirLim_classical
-    (disp : unit) (I : dirType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj i -> Obj j)
+    disp (I : dirType disp)
+    (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj i -> Obj j)
     (Sys : is_dirsys bonding)
   dlT of Choice dlT := {
     dirlim_inj i : Obj i -> dlT;
@@ -57,9 +56,8 @@ HB.factory Record isDirLim_classical
         ind =1 dirlim_ind T f Hcone
   }.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj i -> Obj j)
+    disp (I : dirType disp)
+    (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj i -> Obj j)
     (Sys : is_dirsys bonding)
   dlT of isDirLim_classical disp I Obj bonding Sys dlT.
 
@@ -118,7 +116,7 @@ HB.end.
 
 Section DirSysCongr.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> Type.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -181,13 +179,13 @@ Open Scope ring_scope.
 
 
 HB.factory Record DirLim_isUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -221,13 +219,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isComUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -240,13 +238,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isIDomainDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -263,13 +261,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isFieldDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -293,7 +291,7 @@ Open Scope quotient_scope.
 
 Section Implem.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> choiceType.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -309,7 +307,7 @@ Notation "{ 'dirlim' S }" := (dirlim S).
 
 Section DirectLimitTheory.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> choiceType.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -377,7 +375,7 @@ Open Scope ring_scope.
 
 Section Instances.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 
 Section NModule.
 Variable Obj : I -> nmodType.
@@ -516,7 +514,7 @@ End Instances.
 
 Section TestComUnitAlg.
 Variable (R : comRingType).
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> comUnitAlgType R.
 Variable bonding : forall i j, (i <= j)%O -> {lrmorphism Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.