Removed strange :: in Order class

math-comp · Jan 31, 2024 · f8c5879 · f8c5879
1 parent 91a5b23
commit f8c5879
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/3rdparty/ALEA/Ccpo.v b/3rdparty/ALEA/Ccpo.v
@@ -19,9 +19,9 @@ Delimit Scope O_scope with O.
 Definition eq_rel {A} (E1 E2:relation A) := forall x y, E1 x y <-> E2 x y.
 
 Class Order {A} (E:relation A)  (R:relation A) :=
-  {reflexive :: Reflexive R;
+  {reflexive : Reflexive R;
    order_eq : forall x y, R x y /\ R y x <-> E x y;
-   transitive :: Transitive R }.
+   transitive : Transitive R }.
 
 Generalizable Variables A E R.