From e4b57b24f0a4dc39a8bcc1d13c62d45648b85a23 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 3 Nov 2023 23:13:44 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/17576 (#1698)

---
 src/Curves/Montgomery/XZ.v | 2 +-
 src/Util/FSets/FMapProd.v  | 4 ++--
 src/Util/FSets/FMapTrie.v  | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v
index 17db43d98e..5b6a965497 100644
--- 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
index ce3deb38f0..6a4444e172 100644
--- 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
index 0a349eb580..de4f0f1e0a 100644
--- 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.