Merge pull request #42 from coq-community/coq_18590

Adapt to coq/coq#18590

Author: palmskog

theories/Classes.v

@@ -25,7 +25,7 @@ Class Graph := {
   T: Type;
   X: T -> T -> Type;
   equal: forall A B, relation (X A B);
-  equal_:> forall A B, Equivalence (equal A B)
+  equal_:: forall A B, Equivalence (equal A B)
 }.
 
 (*Arguments equal : simpl never.*)
@@ -91,31 +91,31 @@ Section Structures.
   Context {Mo: Monoid_Ops G} {SLo: SemiLattice_Ops G} {Ko: Star_Op G} {Co: Converse_Op G}.
 
   Class Monoid := {
-    dot_compat:> forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
+    dot_compat:: forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
     dot_assoc: forall A B C D (x: X A B) y (z: X C D), x*(y*z) == (x*y)*z;
     dot_neutral_left:  forall A B (x: X A B), 1*x == x;
     dot_neutral_right:  forall A B (x: X B A), x*1 == x
   }.
 
   Class SemiLattice := {
-    plus_compat:> forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B);
+    plus_compat:: forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B);
     plus_neutral_left: forall A B (x: X A B), 0+x == x;
     plus_idem: forall A B (x: X A B), x+x == x;
     plus_assoc: forall A B (x y z: X A B), x+(y+z) == (x+y)+z;
     plus_com: forall A B (x y: X A B), x+y == y+x
   }.
 
   Class IdemSemiRing := {
-    ISR_Monoid :> Monoid;
-    ISR_SemiLattice :> SemiLattice;
+    ISR_Monoid :: Monoid;
+    ISR_SemiLattice :: SemiLattice;
     dot_ann_left:  forall A B C (x: X B C), zero A B * x == 0;
     dot_ann_right: forall A B C (x: X C B), x * zero B A == 0;
     dot_distr_left:  forall A B C (x y: X A B) (z: X B C), (x+y)*z == x*z + y*z;
     dot_distr_right: forall A B C (x y: X B A) (z: X C B), z*(x+y) == z*x + z*y
   }.
 
   Class KleeneAlgebra := {
-    KA_ISR :> IdemSemiRing;
+    KA_ISR :: IdemSemiRing;
     star_make_left: forall A (a:X A A), 1 + a#*a == a#;
     star_destruct_left: forall A B (a: X A A) (c: X A B), a*c <== c  ->  a#*c <== c;
     star_destruct_right: forall A B (a: X A A) (c: X B A), c*a <== c  ->  c*a# <== c
@@ -127,12 +127,12 @@ Section Structures.
   (* TODO: introduce an intermediate ConverseMonoid class *)
 
   Class ConverseIdemSemiRing := {
-    CISR_SL :> SemiLattice;
+    CISR_SL :: SemiLattice;
     dot_compat_c: forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
     dot_assoc_c: forall A B C D (x: X A B) y (z: X C D), x*(y*z) == (x*y)*z;
     dot_neutral_left_c:  forall A B (x: X A B), 1*x == x;
 
-    conv_compat:> forall A B, Proper (equal A B ==> equal B A) (conv A B);
+    conv_compat:: forall A B, Proper (equal A B ==> equal B A) (conv A B);
     conv_invol: forall A B (x: X A B), x`` == x;
     conv_dot:  forall A B C (x: X A B) (y: X B C), (x*y)` == y`*x`;
     conv_plus:  forall A B (x y: X A B), (x+y)` == y`+x`;
@@ -141,7 +141,7 @@ Section Structures.
   }.
 
   Class ConverseKleeneAlgebra := {
-    CKA_CISR :> ConverseIdemSemiRing;
+    CKA_CISR :: ConverseIdemSemiRing;
     star_make_left_c: forall A (a:X A A), 1 + a#*a == a#;
     star_destruct_left_c: forall A B (a: X A A) (c: X A B), a*c <== c  ->  a#*c <== c
   }.

theories/DKA_DFA_Equiv.v

@@ -182,7 +182,7 @@ Section correctness.
 
   Class invariant tarjan : Prop := 
     {
-      i_wf_tarjan :> DS.WF tarjan ; 
+      i_wf_tarjan :: DS.WF tarjan ;
       i_final : forall x y, {{tarjan}} x y -> final x = final y 
     }.
 

theories/Functors.v

@@ -36,13 +36,13 @@ Section Defs.
     forall A B y, exists x, F A B x == y.
 
   Class monoid_functor {Mo1: Monoid_Ops G1} {Mo2: Monoid_Ops G2} (F: functor G1 G2) := {
-    monoid_graph_functor :> graph_functor F;
+    monoid_graph_functor :: graph_functor F;
     functor_dot : forall A B C x y, F A C (x*y) == F A B x * F B C y;
     functor_one : forall A, F A A 1 == 1
   }.
 
   Class semilattice_functor {SLo1: SemiLattice_Ops G1} {SL2: SemiLattice_Ops G2} (F: functor G1 G2) := {
-    semilattice_graph_functor :> graph_functor F;
+    semilattice_graph_functor :: graph_functor F;
     functor_plus : forall A B x y, F A B (x+y) == F A B x + F A B y;
     functor_zero : forall A B, F A B 0 == 0
   }.
@@ -71,8 +71,8 @@ Section Defs.
     {Ko1: Star_Op G1} {Ko2: Star_Op G2}.
 
   Class semiring_functor (F: functor G1 G2) := {
-    semiring_monoid_functor :> monoid_functor F;
-    semiring_semilattice_functor :> semilattice_functor F
+    semiring_monoid_functor :: monoid_functor F;
+    semiring_semilattice_functor :: semilattice_functor F
   }.
 
   Lemma functor_star_leq {KA1: KleeneAlgebra G1} {KA2: KleeneAlgebra G2} 
@@ -88,7 +88,7 @@ Section Defs.
   Qed.
 
   Class kleene_functor (F: functor G1 G2) := {
-    kleene_semiring :> semiring_functor F;
+    kleene_semiring :: semiring_functor F;
     functor_star: forall A a, F A A (a#) == (F A A a) #
   }.
 

theories/StrictKleeneAlgebra.v

@@ -41,9 +41,9 @@ Delimit Scope SA_scope with SA.
 
 (** Strict Kleene Algebras axioms *)
 Class StrictKleeneAlgebra {G: Graph} {Ops: SKA_Ops G} := {
-  dot_compat:> 
+  dot_compat::
     forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
-  plus_compat:> 
+  plus_compat::
     forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B);
   dot_assoc: forall A B C D (x: X A B) y (z: X C D), x*(y*z) == (x*y)*z;
   dot_neutral_left:  forall A B (x: X A B), 1*x == x;