Adapt to coq/coq#17576

coq-community · Nov 7, 2023 · 2f7f8f2 · 2f7f8f2
1 parent 80013ad
commit 2f7f8f2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/theories/core/checkpoint.v b/theories/core/checkpoint.v
@@ -45,7 +45,7 @@ Section CheckPoints.
 
   Hypothesis G_conn' : connected [set: G].
   Let G_conn : forall x y:G, connect sedge x y.
-  Proof using G_conn'. exact: connectedTE. Qed.
+  Proof. clear -G_conn'. exact: connectedTE. Qed.
 
   Lemma cp_sym x y : cp x y = cp y x.
   Proof using.

diff --git a/theories/planar/hmap_ops.v b/theories/planar/hmap_ops.v
@@ -1103,14 +1103,14 @@ Definition del_node := Hypermap del_node_can3.
 Hypothesis plainG : plain G.
 
 Let NP x : reflect (cnode z x || cnode z (edge x)) (x \in N).
-Proof using plainG.
-apply: (iffP (closureP _ _ _)) => [[y /=]|]; last first.
+Proof.
+clear -plainG; apply: (iffP (closureP _ _ _)) => [[y /=]|]; last first.
   by case/orP; [exists x|exists (edge x); rewrite // -cedge1r].
 by rewrite plain_orbit // !inE => zy /pred2P [?|?]; subst y; rewrite zy.
 Qed.
 
 Let edgeN x : edge x \in N = (x \in N). 
-Proof using. symmetry. apply: closure_closed => //=. exact: cedgeC. Qed.
+Proof. clear. symmetry. apply: closure_closed => //=. exact: cedgeC. Qed.
 
 Lemma del_node_cnode (u v : del_node) : cnode u v = cnode (val u) (val v).
 Proof. by rewrite fconnect_frestrict fconnect_skip //; apply: valP. Qed.