diff --git a/3rdparty/ALEA/Ccpo.v b/3rdparty/ALEA/Ccpo.v index f0668fb..54579d3 100644 --- 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.