Fix coqdev compilation (#44)

* updating to coqdev * preparing v2.0 for release --------- Co-authored-by: Aleksandar Nanevski <[email protected]>
imdea-software · Sep 18, 2024 · 27560ef · 27560ef
1 parent a7c3e04
commit 27560ef
Show file tree

Hide file tree

Showing 5 changed files with 63 additions and 49 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -1,6 +1,10 @@
 -Q . pcm
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
+# release-specific args
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
 
 core/options.v
 core/axioms.v

diff --git a/core/pred.v b/core/pred.v
@@ -1521,7 +1521,7 @@ Definition id_rel : Rel A := fun x y => y = x.
 Lemma id_rel_refl : forall x, id_rel x x.
 Proof. by []. Qed.
 Lemma id_rel_sym : Symmetric id_rel.
-Proof. by []. Qed.
+Proof. by split. Qed.
 Lemma id_rel_trans : Transitive id_rel.
 Proof. by move=> x y z ->->. Qed.
 Lemma id_rel_func : functional id_rel.

diff --git a/core/prelude.v b/core/prelude.v
@@ -1274,7 +1274,7 @@ Lemma onth_tnth {n} (s : n.-tuple A) (i : 'I_n) :
 Proof.
 elim: n s i =>[|n IH] s i; first by case: i.
 case/tupleP: s=>/=x s; case: (unliftP ord0 i)=>[j|]-> /=.
-- by rewrite tnthS.
+- by rewrite tnthS ?add0n.
 by rewrite tnth0.
 Qed.
 

diff --git a/core/slice.v b/core/slice.v
@@ -20,7 +20,7 @@ Open Scope order_scope.
 Import Order.Theory.
 
 Section BSimp_Extension.
-Variables (disp : unit) (T : porderType disp).
+Context disp (T : porderType disp).
 Implicit Types (x y : T) (b c : bool).
 
 Lemma binf_inf b c : (BInfty T b == BInfty T c) = (b == c).

diff --git a/pcm/morphism.v b/pcm/morphism.v
@@ -1571,22 +1571,26 @@ HB.instance Definition _ :=
   isFull_PCM_morphism.Build U W (g \o f) comp_is_full_morphism.
 End FullCompIsFull.
 
-(* instances for combinations must be declared explicitly *)
-
-HB.instance Definition _ (f : full_norm_pcm_morph U V) 
-                         (g : full_norm_pcm_morph V W) :=
-  Full_Norm_PCM_morphism.copy (g \o f) 
-    (Full_Norm_PCM_morphism.pack_ 
-       (Norm_PCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))).
-
-HB.instance Definition _ (f : full_binorm_pcm_morph U V) 
-                         (g : full_binorm_pcm_morph V W) :=
-  Full_Binorm_PCM_morphism.copy (g \o f) 
-    (Full_Binorm_PCM_morphism.pack_ 
-       (Binorm_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))).
+(* instances for combinations must declare PCM_morphism.on *)
+(* before declaring fullness structure. *)
+
+HB.instance Definition _  
+    (f : full_norm_pcm_morph U V) 
+    (g : full_norm_pcm_morph V W) := 
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_norm_pcm_morph U V) 
+    (g : full_norm_pcm_morph V W) := 
+  Full_Norm_PCM_morphism.on (g \o f).
+
+HB.instance Definition _ 
+    (f : full_binorm_pcm_morph U V) 
+    (g : full_binorm_pcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_binorm_pcm_morph U V) 
+    (g : full_binorm_pcm_morph V W) :=
+  Full_Binorm_PCM_morphism.on (g \o f).
 
 End CompMorphism.
 
@@ -1811,43 +1815,49 @@ End CompTPCM.
 (* combinations declared explicitly *)
 
 HB.instance Definition _ 
-  (f : norm_tpcm_morph U V) (g : norm_tpcm_morph V W) :=
-  Norm_TPCM_morphism.copy (g \o f) 
-    (Norm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
-
+    (f : norm_tpcm_morph U V) 
+    (g : norm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
 HB.instance Definition _ 
-  (f : binorm_tpcm_morph U V) (g : binorm_tpcm_morph V W) :=
-  Binorm_TPCM_morphism.copy (g \o f) 
-    (Binorm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
+    (f : norm_tpcm_morph U V) 
+    (g : norm_tpcm_morph V W) :=
+  Norm_TPCM_morphism.on (g \o f).
 
 HB.instance Definition _ 
-  (f : full_tpcm_morph U V) (g : full_tpcm_morph V W) :=
-  Full_TPCM_morphism.copy (g \o f) 
-    (Full_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))).
+    (f : binorm_tpcm_morph U V) 
+    (g : binorm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : binorm_tpcm_morph U V) 
+    (g : binorm_tpcm_morph V W) :=
+  Binorm_TPCM_morphism.on (g \o f).
 
 HB.instance Definition _ 
-  (f : full_norm_tpcm_morph U V) (g : full_norm_tpcm_morph V W) :=
-  Full_Norm_TPCM_morphism.copy (g \o f) 
-    (Full_Norm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
+    (f : full_tpcm_morph U V) 
+    (g : full_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_tpcm_morph U V) 
+    (g : full_tpcm_morph V W) :=
+  Full_TPCM_morphism.on (g \o f).
 
 HB.instance Definition _ 
-  (f : full_binorm_tpcm_morph U V) (g : full_binorm_tpcm_morph V W) :=
-  Full_Binorm_TPCM_morphism.copy (g \o f) 
-    (Full_Binorm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
+    (f : full_norm_tpcm_morph U V) 
+    (g : full_norm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_norm_tpcm_morph U V) 
+    (g : full_norm_tpcm_morph V W) :=
+  Full_Norm_TPCM_morphism.on (g \o f).
+
+HB.instance Definition _  
+    (f : full_binorm_tpcm_morph U V) 
+    (g : full_binorm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_binorm_tpcm_morph U V) 
+    (g : full_binorm_tpcm_morph V W) :=
+  Full_Binorm_TPCM_morphism.on (g \o f).
 
 End Comp.