Merge pull request #39 from coq-community/fix-have-opaque

avoid opaqueness of have in Coq 8.20 and later
coq-community · Jun 26, 2024 · 080d923 · 080d923
2 parents f047a60 + c443888
commit 080d923
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 29 deletions.
diff --git a/theories/core/finmap_plus.v b/theories/core/finmap_plus.v
@@ -219,12 +219,12 @@ Proof.
     if x is Some z then Sub (val (f z)) (fset1Ur (valP (f z))) else Sub e fset1U1.
   pose g_inv  (x : e |` E) : option T := 
     match fsetULVR (valP x) with inl _ => None | inr p => Some (f^-1 (Sub (val x) p)) end.
-  have can_g : cancel g g_inv.
+  have @can_g : cancel g g_inv.
   { move => [x|]; rewrite /g/g_inv/=; case: (fsetULVR _) => [|p] //=. 
     - by rewrite inE fsval_eqF.
     - by rewrite valK' bijK.
     -  exfalso. by rewrite p in He. }
-  have can_g_inv : cancel g_inv g.
+  have @can_g_inv : cancel g_inv g.
   { move => [x Hx]; rewrite /g/g_inv/=. case: (fsetULVR _) => [|p] //=. 
     - rewrite !inE => A. apply: val_inj => /=. by rewrite (eqP A).
     - apply: val_inj => //=. by rewrite bijK'. }
@@ -243,12 +243,12 @@ Proof.
     if x is inl z then Sub (val (f z)) (fset1Ur (valP (f z))) else Sub e fset1U1.
   pose g_inv  (x : e |` E) : T + unit := 
     match fsetULVR (valP x) with inl _ => inr tt | inr p => inl (f^-1 (Sub (val x) p)) end.
-  have can_g : cancel g g_inv.
+  have @can_g : cancel g g_inv.
   { move => [x|[]]; rewrite /g/g_inv/=; case: (fsetULVR _) => [|p] //=. 
     - by rewrite inE fsval_eqF.
     - by rewrite valK' bijK.
     -  exfalso. by rewrite p in He. }
-  have can_g_inv : cancel g_inv g.
+  have @can_g_inv : cancel g_inv g.
   { move => [x Hx]; rewrite /g/g_inv/=. case: (fsetULVR _) => [|p] //=. 
     - rewrite !inE => A. apply: val_inj => /=. by rewrite (eqP A).
     - apply: val_inj => //=. by rewrite bijK'. }
@@ -265,18 +265,18 @@ Definition bij_setD (aT : finType) (C : choiceType) (rT : {fset C}) (A : {set aT
   bij { x | x \in ~: A} (rT `\` [fset val (f x) | x in A]).
 Proof.
   set aT' := ({ x | _ }). set rT' := _ `\` _.
-  have g_proof (x : aT') : val (f (val x)) \in rT'.
+  have @g_proof (x : aT') : val (f (val x)) \in rT'.
   { rewrite !inE (valP (f (val x))) andbT. apply: contraTN (valP x).
     case/imfsetP => /= x0 inA /val_inj /(@bij_injective _ _ f) ->. by rewrite inE negbK. }
   pose g (x : aT') : rT' := Sub (val (f (val x))) (g_proof x).
-  have g_inv_proof (x : rT') :  f^-1 (Sub (fsval x) (fsetDEl x)) \in ~: A.
+  have @g_inv_proof (x : rT') :  f^-1 (Sub (fsval x) (fsetDEl x)) \in ~: A.
   { rewrite inE. case/fsetDP: (valP x) => ?. apply: contraNN => X. apply/imfsetP.
     exists (f^-1 (Sub (fsval x) (fsetDEl x))) => //. by rewrite bijK'. }
   pose g_inv (x : rT') : aT' := Sub (f^-1 (Sub (val x) (fsetDEl x))) (g_inv_proof x). 
-  have can1 : cancel g g_inv.
+  have @can1 : cancel g g_inv.
   { move => [x Hx]. rewrite /g/g_inv. apply: val_inj => /=. apply: (@bij_injective _ _ f).
     rewrite bijK'. exact: val_inj. }
-  have can2 : cancel g_inv g.
+  have @can2 : cancel g_inv g.
   { move => [x Hx]. rewrite /g/g_inv. apply: val_inj => /=. by rewrite bijK'. }
   apply: Bij can1 can2.
 Defined.

diff --git a/theories/core/sgraph.v b/theories/core/sgraph.v
@@ -144,24 +144,24 @@ End InducedSubgraph.
 Lemma induced_isubgraph (G : sgraph) (A : {set G}) : induced A ⇀ G.
 Proof.
 pose f (x : induced A) : G := val x.
-have : {mono f : x y / x -- y} by abstract by move => x y; rewrite induced_edge.
-apply: ISubgraph; exact: val_inj.
+have @H : {mono f : x y / x -- y} by abstract by move => x y; rewrite induced_edge.
+move: H; apply: ISubgraph; exact: val_inj.
 Defined.
 
 Lemma isubgraph_induced (F G : sgraph) (i : F ⇀ G) : 
   F ≃ induced [set x in codom i].
 Proof.
 set A := [set _ in _].
-have jP (x : induced A) : val x \in codom i. 
+have @jP (x : induced A) : val x \in codom i.
   abstract by move: (valP x); rewrite inE.
 pose j (x : induced A) : F := iinv (jP x).
-have iP (x : F) : i x \in A by abstract by rewrite inE codom_f.
+have @iP (x : F) : i x \in A by abstract by rewrite inE codom_f.
 pose i' (x : F) : induced A := Sub (i x) (iP x).
-have can_i : cancel i' j. 
+have @can_i : cancel i' j.
   abstract by move=> x; apply: (isubgraph_inj i); rewrite f_iinv.
-have can_j : cancel j i'. 
+have @can_j : cancel j i'.
   abstract by move => [x xA]; apply: val_inj; rewrite /j/=f_iinv.
-apply: Diso' can_i can_j _. 
+apply: Diso' can_i can_j _.
   abstract by move => x y; rewrite induced_edge /= isubgraph_mono.
 Defined.
 
@@ -1443,7 +1443,7 @@ Qed.
 
 Lemma isubgraph_complLR (F G : sgraph) (i : compl F ⇀ G) : F ⇀ compl G.
 Proof.
-have I := isubgraph_inj i; apply: (@ISubgraph F (compl G) i) => // x y.
+have @I := isubgraph_inj i; apply: (@ISubgraph F (compl G) i) => // x y.
 exact: isubgraph_compLR_mono.
 Defined.
 

diff --git a/theories/core/transfer.v b/theories/core/transfer.v
@@ -574,7 +574,7 @@ Qed.
 Lemma open_add_edge (x y : G) u : 
   open (G ∔ [x, u, y]) ⩭2 open G ∔ [inj_v x, u, inj_v y].
 Proof. 
-  have X : is_graph (add_edge (open G) (inj_v x) u (inj_v y)). 
+  have @X : is_graph (add_edge (open G) (inj_v x) u (inj_v y)).
   { exact: add_edge_graph. }
   econstructor.
   apply: iso2_comp (iso2_sym _) _. apply: openK.
@@ -651,21 +651,21 @@ Proof.
   move: j => [isF isG i] Vz IOz /=.
   unshelve econstructor. 
   { apply remove_vertex_graph => //; constructor. rewrite (oiso2_pIO (OIso2 i)) // in IOz. }
-  have E1 : [fset vfun_body i z] = [fset val (i x) | x : vset F & val x \in [fset z]]. (* : / in?? *)
+  have @E1 : [fset vfun_body i z] = [fset val (i x) | x : vset F & val x \in [fset z]]. (* : / in?? *)
   { apply/fsetP => k. rewrite inE vfun_bodyE. apply/eqP/imfsetP => /= [->|[x] /= ].
     - exists (Sub z Vz) => //. by rewrite !inE.
     - rewrite !inE => /eqP X ->. move: Vz. rewrite -X => Vz. by rewrite fsvalK. }
-  have E2 : edges_at G (vfun_body i z) = [fset val (i.e x) | x : eset F & val x \in edges_at F z].
+  have @E2 : edges_at G (vfun_body i z) = [fset val (i.e x) | x : eset F & val x \in edges_at F z].
   { rewrite (@oiso2_edges_at _ _ (OIso2 i)) //=. apply/fsetP => k. apply/imfsetP/imfsetP.
     - case => /= x Ix ->. 
-      have Hx : x \in eset F. move: Ix. rewrite edges_atE. by case: (_ \in _).
+      have @Hx : x \in eset F. move: Ix. rewrite edges_atE. by case: (_ \in _).
       exists (Sub x Hx) => //. by rewrite efun_bodyE. 
     - case => /= x. rewrite inE => Hx ->. exists (fsval x) => //. by rewrite efun_bodyE fsvalK. }
-  - have P e (p : e \in eset (F \ z)) : val (i.e (Sub e (fsetDl p))) \in eset G `\` edges_at G (vfun_body i z).
+  - have @P e (p : e \in eset (F \ z)) : val (i.e (Sub e (fsetDl p))) \in eset G `\` edges_at G (vfun_body i z).
     { rewrite inE [_ \in eset G]valP andbT E2. apply: contraTN (p).
       case/imfsetP => /= e0. rewrite inE => A. move/val_inj. move/(@bij_injective _ _ i.e) => ?; subst.
       by rewrite inE A. }
-    have Q v (p : v \in vset (F \ z)) : val (i (Sub v (fsetDl p))) \in vset G `\ vfun_body i z.
+    have @Q v (p : v \in vset (F \ z)) : val (i (Sub v (fsetDl p))) \in vset G `\ vfun_body i z.
     { rewrite inE [_ \in vset G]valP andbT E1. apply: contraTN (p).
       case/imfsetP => /= v0. rewrite inE => A. move/val_inj. move/(@bij_injective _ _ i) => ?; subst.
       by rewrite inE A. }
@@ -713,8 +713,8 @@ Lemma oiso2_add_edge (F G : pre_graph) (i : F ⩭2 G) e1 e2 x y u v :
   F ∔ [e1,x,u,y] ⩭2 G ∔ [e2,i x,v,i y].
 Proof.
   case: i => isF isG i fresh_e1 fresh_e2 Vx Vy uv /=.
-  have isF' : is_graph (F ∔ [e1, x, u, y]) by abstract exact: add_edge_graph'.
-  have isG' : is_graph (G ∔ [e2, vfun_body i x, v, vfun_body i y]).
+  have @isF' : is_graph (F ∔ [e1, x, u, y]) by abstract exact: add_edge_graph'.
+  have @isG' : is_graph (G ∔ [e2, vfun_body i x, v, vfun_body i y]).
     by abstract (apply: add_edge_graph'; exact: (oiso2_vset (OIso2 i))).
   econstructor.
   apply: iso2_comp. apply: pack_add_edge'. assumption. 
@@ -728,13 +728,13 @@ Lemma oiso2_remove_edges (F G : pre_graph) (i : F ⩭2 G) E E':
   E' = [fset efun_of i e | e in E] -> (F - E) ⩭2 (G - E').
 Proof.
   case: i => isF isG i /= S EE'. econstructor.
-  have X :  E' = [fset val (i.e x) | x : eset F & val x \in E].
+  have @X :  E' = [fset val (i.e x) | x : eset F & val x \in E].
   { subst. apply/fsetP => k. apply/imfsetP/imfsetP.
     - case => /= x Ix ->.  
-      have Hx : x \in eset F. move: Ix. apply: (fsubsetP S). 
+      have @Hx : x \in eset F. move: Ix. apply: (fsubsetP S).
       exists (Sub x Hx) => //. by rewrite efun_bodyE. 
     - case => /= x. rewrite inE => Hx ->. exists (fsval x) => //. by rewrite efun_bodyE fsvalK. }
-  have P e (p : e \in eset (F - E)) : val (i.e (Sub e (fsetDl p))) \in eset G `\` E'.
+  have @P e (p : e \in eset (F - E)) : val (i.e (Sub e (fsetDl p))) \in eset G `\` E'.
   { rewrite inE [_ \in eset G]valP andbT X. apply: contraTN (p).
     case/imfsetP => /= e0. rewrite inE => A. move/val_inj. move/(@bij_injective _ _ i.e) => ?; subst.
     by rewrite inE A. }
@@ -775,8 +775,8 @@ Lemma oiso2_add_edge' (F G : pre_graph) (i : F ⩭2 G)
 Proof with eauto with typeclass_instances.
   case: i => isF isG i.
   move => E1 E2 Vx Vy Vx' Vy' Ix Iy uv. 
-  have isF' : is_graph ( F ∔ [e1, x, u, y] ). apply add_edge_graph'...
-  have isG' : is_graph (  G ∔ [e2, x', v, y']). apply add_edge_graph'...
+  have @isF' : is_graph ( F ∔ [e1, x, u, y] ). apply add_edge_graph'...
+  have @isG' : is_graph (  G ∔ [e2, x', v, y']). apply add_edge_graph'...
   econstructor. 
   apply: iso2_comp. apply: pack_add_edge'. assumption.
   apply: iso2_comp (iso2_sym _). 2: apply: pack_add_edge'; try assumption.