Adapt to coq/coq#17576 (#1698)

mit-plv · Nov 3, 2023 · e4b57b2 · e4b57b2
1 parent 5f1aae0
commit e4b57b2
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v
@@ -37,7 +37,7 @@ Module M.
       end.
 
     Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
-    Proof using char_ge_5. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+    Proof. clear -char_ge_5. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
 
     (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *)
     Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.

diff --git a/src/Util/FSets/FMapProd.v b/src/Util/FSets/FMapProd.v
@@ -671,7 +671,7 @@ Module ProdWSfun_gen (E1 : DecidableTypeOrig) (E2 : DecidableTypeOrig) (M1 : WSf
       Proof using Type. clear; cbv [In]; setoid_rewrite find_iff; setoid_rewrite remove_full; spec_t. Qed.
       Let elements_iff :
         InA (@eq_key_elt _) (x,e) (elements m) <-> MapsTo x e m.
-      Proof using Type.
+      Proof.
         clear; cbv [MapsTo elements].
         setoid_rewrite M1'.elements_mapsto_iff.
         setoid_rewrite M2'.elements_mapsto_iff.
@@ -717,7 +717,7 @@ Module ProdWSfun_gen (E1 : DecidableTypeOrig) (E2 : DecidableTypeOrig) (M1 : WSf
 
       Variable cmp : elt -> elt -> bool.
       Let equal_iff : Equivb cmp m m' <-> equal cmp m m' = true.
-      Proof using Type.
+      Proof.
         clear; cbv [equal Equivb] in *.
         rewrite Equiv_alt_iff, <- M1'.equal_iff.
         cbv [Equiv_alt M1.Equivb Cmp].

diff --git a/src/Util/FSets/FMapTrie.v b/src/Util/FSets/FMapTrie.v
@@ -1376,7 +1376,7 @@ Module Import ListWSfun_gen_proofs.
 
       Let elements_iff :
         MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m).
-      Proof using Type.
+      Proof.
         clear; cbv [MapsTo].
         rewrite InA_alt.
         cbv [eq_key_elt]; cbn [fst snd].
@@ -1645,7 +1645,7 @@ Module Import ListWSfun_gen_proofs.
       Variable cmp : elt -> elt -> bool.
 
       Let equal_iff : equal cmp m m' = true <-> Equivb cmp m m'.
-      Proof using Type.
+      Proof.
         clear; cbv [equal Equivb] in *.
         cbv [Equiv In Cmp].
         setoid_rewrite find_iff.