MathComp 2.3 compat

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) $<

README.md

@@ -163,15 +163,15 @@ Installation
 This library is based on
 
 * [SSReflect/MathComp 2]([https://github.com/math-comp/math-comp])
-  Library version 2.2.0 or more recent.
+  Library version 2.3.0 or more recent.
 
 Here are the Opam packages I'm using
 ```
-coq-hierarchy-builder        1.7.0
-coq-mathcomp-ssreflect       2.2.0
-coq-mathcomp-algebra         2.2.0
-coq-mathcomp-field           2.2.0
-coq-mathcomp-fingroup        2.2.0
-coq-mathcomp-character       2.2.0
-coq-mathcomp-multinomials    2.2.0
+coq-hierarchy-builder        1.8.0
+coq-mathcomp-ssreflect       2.3.0
+coq-mathcomp-algebra         2.3.0
+coq-mathcomp-field           2.3.0
+coq-mathcomp-fingroup        2.3.0
+coq-mathcomp-character       2.3.0
+coq-mathcomp-multinomials    2.3.0
 ```

_CoqProject

@@ -1,6 +1,7 @@
 -docroot Combi
 -R theories Combi
 -arg -w -arg -notation-overridden
+-arg -w -arg -notation-incompatible-prefix
 -arg -w -arg -ambiguous-paths
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant

theories/Basic/ordtype.v

@@ -55,7 +55,7 @@ Import Order.Theory.
 (** * Induction on partially ordered types                                    *)
 (******************************************************************************)
 
-Lemma finord_wf (disp : unit) (T : finPOrderType disp) (P : T -> Type) :
+Lemma finord_wf disp (T : finPOrderType disp) (P : T -> Type) :
   (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.
 Proof.
 move=> IH x.
@@ -67,7 +67,7 @@ rewrite -{}eqcn; apply proper_card; apply/andP; split; apply/subsetP.
 - by move/(_ y); rewrite !inE => /(_ ltxy); rewrite ltxx.
 Qed.
 
-Lemma finord_wf_down (disp : unit) (T : finPOrderType disp) (P : T -> Type) :
+Lemma finord_wf_down disp (T : finPOrderType disp) (P : T -> Type) :
   (forall x, (forall y, y > x -> P y) -> P x) -> forall x, P x.
 Proof. exact: (finord_wf (T := T^d : finPOrderType _)). Qed.
 
@@ -78,12 +78,12 @@ Proof. exact: (finord_wf (T := T^d : finPOrderType _)). Qed.
 
 (** We only define covering relation for finite type, since it cannot be      *)
 (** decided and it is not very useful for infinite orders.                    *)
-Definition covers {disp : unit} {T : finPOrderType disp} :=
+Definition covers {disp} {T : finPOrderType disp} :=
   [rel x y : T | (x < y) && [forall z, ~~(x < z < y)]].
 
 Section CoversFinPOrder.
 
-Variable (disp : unit) (T : finPOrderType disp).
+Variable (disp : _) (T : finPOrderType disp).
 Implicit Type (x y : T).
 
 Lemma coversP x y : reflect (x < y /\ (forall z, ~(x < z < y))) (covers x y).
@@ -148,7 +148,7 @@ Proof. by rewrite -covers_connect; apply: (iffP connectP). Qed.
 
 End CoversFinPOrder.
 
-Lemma covers_rind (disp : unit) (T : finPOrderType disp) (P : T -> Type) :
+Lemma covers_rind disp (T : finPOrderType disp) (P : T -> Type) :
   (forall x y, covers y x -> P x -> P y) ->
   forall x, P x -> forall y, x >= y -> P y.
 Proof.
@@ -168,12 +168,12 @@ HB.structure Definition Inhabited := {T of isInhabited T & Choice T}.
 
 HB.factory Record isInhabitedType T := { x : T }.
 HB.builders Context T of isInhabitedType T.
-HB.instance Definition _ :=  isInhabited.Build T (ex_intro _ x is_true_true).
+#[warning="-HB.no-new-instance"]
+HB.instance Definition _ := isInhabited.Build T (ex_intro _ x is_true_true).
 HB.end.
 
 HB.instance Definition _ := isInhabitedType.Build unit tt.
 HB.instance Definition _ := isInhabitedType.Build bool false.
-HB.instance Definition _ := isInhabitedType.Build Prop False.
 HB.instance Definition _ := isInhabitedType.Build nat 0.
 HB.instance Definition _ (n : nat) := isInhabitedType.Build 'I_n.+1 ord0.
 
@@ -207,35 +207,35 @@ HB.structure Definition InhFinite := { T of isInhabited T & Finite T }.
 (** ** Inhabited ordered types                                                *)
 (******************************************************************************)
 #[short(type=inhPOrderType)]
-HB.structure Definition InhPOrder (d : unit) :=
+HB.structure Definition InhPOrder d :=
   {T of isInhabited T & Order.POrder d T}.
 
 #[short(type=inhLatticeType)]
-HB.structure Definition InhLattice (d : unit) :=
+HB.structure Definition InhLattice d :=
   {T of isInhabited T & Order.Lattice d T}.
 
 #[short(type=inhTBLatticeType)]
-HB.structure Definition InhTBLattice (d : unit) :=
+HB.structure Definition InhTBLattice d :=
   {T of isInhabited T & Order.TBLattice d T}.
 
 #[short(type=inhOrderType)]
-HB.structure Definition InhOrder (d : unit) :=
+HB.structure Definition InhOrder d :=
   {T of isInhabited T & Order.Total d T}.
 
 
 (******************************************************************************)
 (** ** Inhabited finite partially ordered types                               *)
 (******************************************************************************)
 #[short(type=inhFinPOrderType)]
-HB.structure Definition InhFinPOrder (d : unit) :=
+HB.structure Definition InhFinPOrder d :=
   {T of isInhabited T & Order.POrder d T & Finite T}.
 
 #[short(type=inhFinLatticeType)]
-HB.structure Definition InhFinLattice (d : unit) :=
+HB.structure Definition InhFinLattice d :=
   {T of isInhabited T & Order.FinLattice d T}.
 
 #[short(type=inhFinOrderType)]
-HB.structure Definition InhFinOrder (d : unit) :=
+HB.structure Definition InhFinOrder d :=
   {T of isInhabited T & Order.FinTotal d T}.
 
 HB.instance Definition _ := Inhabited.on bool.
@@ -246,15 +246,14 @@ Section Dual.
 HB.instance Definition _ (T : inhType) :=
   isInhabitedType.Build (Order.dual T) (@inh T).
 
-Variable d : unit.
-HB.instance Definition _ (T : inhPOrderType d) := InhPOrder.on (T^d).
-HB.instance Definition _ (T : inhLatticeType d) := InhLattice.on (T^d).
-HB.instance Definition _ (T : inhTBLatticeType d) := InhTBLattice.on (T^d).
-HB.instance Definition _ (T : inhOrderType d) := InhOrder.on (T^d).
+HB.instance Definition _ d (T : inhPOrderType d) := InhPOrder.on (T^d).
+HB.instance Definition _ d (T : inhLatticeType d) := InhLattice.on (T^d).
+HB.instance Definition _ d (T : inhTBLatticeType d) := InhTBLattice.on (T^d).
+HB.instance Definition _ d (T : inhOrderType d) := InhOrder.on (T^d).
 
-HB.instance Definition _ (T : inhFinPOrderType d) := InhFinPOrder.on (T^d).
-HB.instance Definition _ (T : inhFinLatticeType d) := InhFinLattice.on (T^d).
-HB.instance Definition _ (T : inhFinOrderType d) := InhFinOrder.on (T^d).
+HB.instance Definition _ d (T : inhFinPOrderType d) := InhFinPOrder.on (T^d).
+HB.instance Definition _ d (T : inhFinLatticeType d) := InhFinLattice.on (T^d).
+HB.instance Definition _ d (T : inhFinOrderType d) := InhFinOrder.on (T^d).
 
 End Dual.
 
@@ -264,7 +263,7 @@ End Dual.
 (** *** Maximum of a sequence *)
 Section MaxSeq.
 
-Variables (disp : unit) (T : orderType disp).
+Variables (disp : _) (T : orderType disp).
 Implicit Type a b c : T.
 Implicit Type u v : seq T.
 
@@ -300,7 +299,7 @@ End MaxSeq.
 (** *** Comparison of the elements of a sequence to an element *)
 Section AllLeqLtn.
 
-Variables (disp : unit) (T : orderType disp).
+Variables (disp : _) (T : orderType disp).
 Implicit Type a b c : T.
 Implicit Type u v : seq T.
 
@@ -453,7 +452,7 @@ End AllLeqLtn.
 (** *** Removing the largest letter of a sequence *)
 Section RemoveBig.
 
-Variables (disp : unit) (T : orderType disp).
+Variables (disp : _) (T : orderType disp).
 Variable Z : T.
 Implicit Type a b c : T.
 Implicit Type u v w r : seq T.

theories/Basic/unitriginv.v

@@ -47,8 +47,7 @@ Import GRing.Theory.
 Section UniTriangular.
 
 Variable R : comUnitRingType.
-Variable disp : unit.
-Variable T : finPOrderType disp.
+Variables (disp : _) (T : finPOrderType disp).
 Implicit Type M : T -> T -> R.
 Implicit Types t u v : T.
 
@@ -151,8 +150,7 @@ End UniTriangular.
 Section TriangularInv.
 
 Variable R : comUnitRingType.
-Variable disp : unit.
-Variable T : finPOrderType disp.
+Variable (disp : _) (T : finPOrderType disp).
 Variable M : T -> T -> R.
 Implicit Types t u v : T.
 

theories/Combi/Dyckword.v

@@ -350,14 +350,17 @@ Canonical join_Dyck D1 D2 := DyckWord (Dyck_word_OwCw D1 D2).
 
 End DyckType.
 
-Notation "[ 'Dyck' 'of' s ]" := (dyck (fun sP => @DyckWord s sP))
+#[warning="-notation-incompatible-prefix"]
+Notation "'[' 'Dyck' 'of' s ]" := (dyck (fun sP => @DyckWord s sP))
   (at level 9, format "[ 'Dyck'  'of'  s ]") : form_scope.
 
-Notation "[ 'Dyck' 'of' s 'by' pf ]" := (@DyckWord s pf)
+#[warning="-notation-incompatible-prefix"]
+Notation "'[' 'Dyck' 'of' s 'by' pf ]" := (@DyckWord s pf)
   (at level 9, format "[ 'Dyck'  'of'  s  'by'  pf ]") : form_scope.
 
-Notation "[ 'Dyck' {{ D1 }} D2 ]" := (join_Dyck D1 D2)
-  (at level 8, format "[ 'Dyck'  {{  D1  }}  D2 ]",
+#[warning="-notation-incompatible-prefix"]
+Notation "'[' 'Dyck' '{{' D1 '}}' D2 ]" := (join_Dyck D1 D2)
+  (at level 8, format "[ 'Dyck'  '{{'  D1  '}}'  D2 ]",
    D1 at next level) : form_scope.
 
 
@@ -467,7 +470,7 @@ Implicit Type D : Dyck.
 
 Variable P : Dyck -> Type.
 Hypotheses (Pnil : P nil_Dyck)
-           (Pcons : forall D1 D2, P D1 -> P D2 -> P ([Dyck {{ D1 }} D2])).
+           (Pcons : forall D1 D2, P D1 -> P D2 -> P [Dyck {{ D1 }} D2]).
 
 Theorem Dyck_ind D : P D.
 Proof.

theories/Combi/bintree.v

@@ -1362,7 +1362,7 @@ apply/anti_leq/andP; split.
 Qed.
 
 
-Fact Tamari_display : unit. Proof. exact: tt. Qed.
+Fact Tamari_display : Order.disp_t. Proof. by []. Qed.
 Notation "x <=T y" := (@Order.le Tamari_display _ x y).
 Notation "x <T y" := (@Order.lt Tamari_display _ x y).
 Notation "x /\T y" := (@Order.meet Tamari_display _ x y).
@@ -1534,9 +1534,9 @@ Proof. by rewrite -Tamari_flip flipsz_rightcomb; exact: leftcomb_bottom. Qed.
 #[export] HB.instance Definition _ :=
   Order.hasTop.Build Tamari_display (bintreesz n) rightcomb_top.
 
-Lemma botETamari : 0%O = leftcombsz n.
+Lemma botETamari : \bot%O = leftcombsz n.
 Proof. by []. Qed.
-Lemma topETamari : 1%O = rightcombsz n.
+Lemma topETamari : \top%O = rightcombsz n.
 Proof. by []. Qed.
 
 

theories/Combi/composition.v

@@ -57,7 +57,7 @@ Unset Printing Implicit Defensive.
 
 
 HB.factory Record IsoBottom disp T of Order.POrder disp T := {
-  disp' : unit;
+  disp' : Order.disp_t;
   T' : bPOrderType disp';
   f : T -> T';
   f' : T' -> T;
@@ -77,7 +77,7 @@ HB.end.
 
 
 HB.factory Record IsoTop disp T of Order.POrder disp T := {
-  disp' : unit;
+  disp' : Order.disp_t;
   T' : tPOrderType disp';
   f : T -> T';
   f' : T' -> T;
@@ -652,7 +652,7 @@ Implicit Types (c : 'CRef) (d : {set 'I_n.-1}).
 
 #[export] HB.instance Definition _ := SubType.copy 'CRef (intcompn n).
 #[export] HB.instance Definition _ := Finite.copy 'CRef (intcompn n).
-Fact compnref_display : unit. Proof. exact: tt. Qed.
+Fact compnref_display : Order.disp_t. Proof. by []. Qed.
 #[export] HB.instance Definition _ : Order.isPOrder compnref_display 'CRef :=
   Order.CanIsPartial compnref_display (@descsetK n).
 #[export] HB.instance Definition _ :=
@@ -696,10 +696,10 @@ Qed.
   IsoTop.Build compnref_display 'CRef
                  (@descsetK n) (@from_descsetK n) descset_mono.
 
-Lemma topEcompnref : 1%O = colcompn n :> 'CRef.
+Lemma topEcompnref : \top%O = colcompn n :> 'CRef.
 Proof. by apply: descset_inj; rewrite from_descsetK descset_colcompn. Qed.
 
-Lemma botEcompnref : 0%O = rowcompn n :> 'CRef.
+Lemma botEcompnref : \bot%O = rowcompn n :> 'CRef.
 Proof. by apply: descset_inj; rewrite from_descsetK descset_rowcompn. Qed.
 
 Lemma compnref_rev c1 c2 :

theories/Combi/multinomial.v

@@ -39,7 +39,8 @@ Implicit Type (i a b : nat) (s t : seq nat).
 Fixpoint multinomial_rec s :=
   if s is i :: s' then 'C(sumn s, i) * (multinomial_rec s') else 1.
 Arguments multinomial_rec : simpl nomatch.
-Definition multinomial := nosimpl multinomial_rec.
+Definition multinomial := multinomial_rec.
+Arguments multinomial : simpl never.
 Notation "''C' [ s ]" := (multinomial s)
   (at level 8, format "''C' [ s ]") : nat_scope.