Merge pull request #22 from coq-community/coq817

Adapt to Coq 8.17
coq-community · Mar 10, 2023 · acaa128 · acaa128
2 parents 3c78861 + 3d2b35c
commit acaa128
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 8 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,13 +17,11 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.10'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/coq-bits.opam b/coq-bits.opam
@@ -19,9 +19,9 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "ocaml" {(>= "4.05" & < "4.15~")}
-  "coq" {(>= "8.10" & < "8.17~")}
+  "coq" {(>= "8.14" & < "8.18~")}
   "ocamlbuild" 
-  "coq-mathcomp-algebra" {(>= "1.12" & < "1.16~")}
+  "coq-mathcomp-algebra" {(>= "1.12" & < "1.17~")}
 ]
 
 tags: [

diff --git a/src/spec/operations/properties.v b/src/spec/operations/properties.v
@@ -366,6 +366,7 @@ apply pow2_sub_ltn.
 rewrite modn_small => //; last apply pow2_gt1.
 Qed.
 
+#[export]
 Hint Rewrite toZp_incB toZp_decB : ZpHom.
 
 (*---------------------------------------------------------------------------
@@ -553,6 +554,7 @@ case E: (toNat p) => [| n'].
   apply pow2_sub_ltn.
 Qed.
 
+#[export]
 Hint Rewrite toZp_negB : ZpHom.
 
 Lemma negBK n : involutive (@negB n).
@@ -646,6 +648,7 @@ rewrite (@modn_small (toNat p2)); last apply toNatBounded.
 by rewrite modn_mod.
 Qed.
 
+#[export]
 Hint Rewrite toZp_adcB toZp_addB : ZpHom.
 
 Lemma addBC n : commutative (@addB n).
@@ -777,6 +780,7 @@ case E: (toNat q) => [| n'].
   done.
 Qed.
 
+#[export]
 Hint Rewrite toZp_subB : ZpHom.
 
 Lemma subB_equiv_addB_negB n (p q: BITS n): subB p q = addB p (negB q).
@@ -1499,6 +1503,7 @@ rewrite natrD natrM.
 by rewrite /toZpAux -Zp_nat.
 Qed.
 
+#[export]
 Hint Rewrite toZp_shlBaux toZp_shlB : ZpHom.
 
 Lemma shlB_dropmsb n (p: BITS n.+1) : shlB (dropmsb p) = dropmsb (shlB p).
@@ -1800,6 +1805,7 @@ rewrite /mulB/toZp. rewrite toNat_low. rewrite toNat_fullmulB.
 rewrite modZp_pow. rewrite -!Zp_nat. by rewrite !natrM.
 Qed.
 
+#[export]
 Hint Rewrite toZp_mulB : ZpHom.
 
 Lemma toNat_mulB n (p1 p2: BITS n) : toNat (mulB p1 p2) = (toNat p1 * toNat p2) %% 2^n.
@@ -2065,6 +2071,7 @@ Add Ring DWORDbooleanring : (BITSbooleanring n32).
 Add Ring BYTEbooleanring : (BITSbooleanring n8).
 
 (* Small hint database for directed "shrinking" rewrites *)
+#[export]
 Hint Rewrite
   decBK incBK decB_zero incB_ones incB_fromNat decB_fromSuccNat
   xorBB xorB0 xor0B xorBN xorBNaux
@@ -2079,7 +2086,6 @@ Hint Rewrite
   shlB_asMul shlB_mul2exp
   shlB_fromNat shrB_fromNat : bitsHints.
 
+#[export]
 Hint Rewrite
   <- addB_addn subB_addn mulB_addn mulB_muln : bitsHints.
-
-
diff --git a/src/spec/spec/properties.v b/src/spec/spec/properties.v
@@ -128,6 +128,7 @@ rewrite /=Zp_cast; last apply pow2_gt1.
 by rewrite modn_mod.
 Qed.
 
+#[export]
 Hint Rewrite toZp_fromNat toZpAux_fromNat : ZpHom.
 
 Lemma toNat_droplsb n (p: BITS n.+1) : toNat (droplsb p) = (toNat p)./2.
@@ -312,6 +313,7 @@ rewrite -subn1. replace (1 %% 2^n.+1) with 1 => //.
 by rewrite modn_small; last apply pow2_gt1.
 Qed.
 
+#[export]
 Hint Rewrite toZpK fromZpK toZp_zero toZpAux_zero toZp_ones : ZpHom.
 
 
@@ -359,6 +361,7 @@ rewrite toNat_dropmsb.
 by rewrite modn_mod.
 Qed.
 
+#[export]
 Hint Rewrite toZp_joinmsb0 toZp_dropmsb : ZpHom.
 
 Lemma splitmsbK n : cancel (@splitmsb n) (@joinmsb n).

diff --git a/src/ssrextra/tuple.v b/src/ssrextra/tuple.v
@@ -40,6 +40,7 @@ Proof.
     by rewrite mapCons IHn.
 Qed.
 
+#[export]
 Hint Rewrite @mapCons @mapNil @theadCons @ beheadCons @zipCons @nseqCons @catCons @catNil @mapId : tuple.
 
 Lemma behead_nseq {n A} (a:A) : behead_tuple (nseq_tuple n.+1 a) = nseq_tuple n a.