Fix deprecation from MathComp 1.15

coq-community · Jun 8, 2023 · 910634f · 910634f
1 parent f555a76
commit 910634f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 11 deletions.
diff --git a/theories/acyclic.v b/theories/acyclic.v
@@ -52,7 +52,7 @@ Coercion equivalence_rel_trans : equivalence_rel >-> transitive.
 
 Notation EquivalenceRel R Req := (EquivRel R Req Req Req).
 
-#[export] Hint Resolve equiv_equivalence_rel.
+#[export] Hint Resolve equiv_equivalence_rel : core.
 
 Section EquivalencePartitionExtra.
 

diff --git a/theories/extra.v b/theories/extra.v
@@ -261,17 +261,17 @@ Variable r : rel V.
 Local Notation "x -[]-> y" :=
   (connect r x y) (at level 10, format "x  -[]->  y") .
 
-Local Notation connect_to s :=  (connect (rel_of_simpl_rel (relto s r))).
+Local Notation connect_to s :=  (connect (rel_of_simpl (relto s r))).
 
 Local Notation "x -[ s ]-> y" := (connect_to s x y)
   (at level 10, format "x  -[ s ]->  y").
 
 Local Notation "x =[]= y" := (symconnect r x y) 
   (at level 10, format "x  =[]=  y").
 
-Local Notation symconnect_to a := (symconnect (rel_of_simpl_rel (relto a r))).
+Local Notation symconnect_to a := (symconnect (rel_of_simpl (relto a r))).
 
-Local Notation "x =[ a ]= y" := (symconnect (rel_of_simpl_rel (relto a r)) x y) 
+Local Notation "x =[ a ]= y" := (symconnect (rel_of_simpl (relto a r)) x y)
   (at level 10, format "x  =[ a ]=  y").
 
 Lemma connect_to1 (a : pred V) x y : y \in a -> r x y -> x -[a]-> y.
@@ -340,4 +340,4 @@ Qed.
 Lemma setUDl (T : finType) (A B : {set T}) : A :|: B :\: A = A :|: B.
 Proof. by apply/setP=> x; rewrite !inE; do !case: (_ \in _). Qed.
 
-End extra_set.
+End extra_set.
diff --git a/theories/kosaraju.v b/theories/kosaraju.v
@@ -20,17 +20,17 @@ Variable r : rel T.
 Local Notation "x -[]-> y" :=
   (connect r x y) (at level 10, format "x  -[]->  y") .
 
-Local Notation connect_to s :=  (connect (rel_of_simpl_rel (relto s r))).
+Local Notation connect_to s :=  (connect (rel_of_simpl (relto s r))).
 
 Local Notation "x -[ s ]-> y" := (connect_to s x y)
   (at level 10, format "x  -[ s ]->  y").
 
 Local Notation "x =[]= y" := (symconnect r x y)
   (at level 10, format "x  =[]=  y").
 
-Local Notation symconnect_to a := (symconnect (rel_of_simpl_rel (relto a r))).
+Local Notation symconnect_to a := (symconnect (rel_of_simpl (relto a r))).
 
-Local Notation "x =[ a ]= y" := (symconnect (rel_of_simpl_rel (relto a r)) x y)
+Local Notation "x =[ a ]= y" := (symconnect (rel_of_simpl (relto a r)) x y)
   (at level 10, format "x  =[ a ]=  y").
 
 Lemma connect_to_C1r x y z :
@@ -175,7 +175,7 @@ Section ConnectRelto.
 Variable r : rel T.
 
 Local Notation "x -[ s ]-> y" :=
-  (connect (rel_of_simpl_rel (relto s r)) x y)
+  (connect (rel_of_simpl (relto s r)) x y)
   (at level 10, format "x  -[ s ]->  y").
 
 Local Notation "x -[]-> y" :=
@@ -184,7 +184,7 @@ Local Notation "x -[]-> y" :=
 Local Notation "x =[]= y" := (symconnect r x y)
   (at level 10, format "x  =[]=  y").
 
-Local Notation "x =[ a ]= y" := (symconnect (rel_of_simpl_rel (relto a r)) x y)
+Local Notation "x =[ a ]= y" := (symconnect (rel_of_simpl (relto a r)) x y)
   (at level 10, format "x  =[ a ]=  y").
 
 Local Notation "C[ x ]_( a , l )" := (can_to r x a l)
@@ -481,7 +481,7 @@ Definition pdfs := rpdfs #|T|.
 Definition tseq := (foldl pdfs (setT, [::]) (enum T)).2.
 
 Local Notation "x -[ l ]-> y" :=
-  (connect (rel_of_simpl_rel (relto l (grel g))) x y)
+  (connect (rel_of_simpl (relto l (grel g))) x y)
   (at level 10, format "x  -[ l ]->  y").
 Local Notation "x -[]-> y" := (connect (grel g) x y)
   (at level 10, format "x  -[]->  y").