ocaml 3.09 transition

[helm.git] / helm / matita / library / higher_order_defs / ordering.ma

diff --git a/helm/matita/library/higher_order_defs/ordering.ma b/helm/matita/library/higher_order_defs/ordering.ma
index a945805da1496d6156602efae9ba3e31e584073d..c2b351d7abe878a4f5064c96410ead6171dc8ffc 100644 (file)
--- a/helm/matita/library/higher_order_defs/ordering.ma
+++ b/helm/matita/library/higher_order_defs/ordering.ma
@@ -18,5 +18,5 @@ include "logic/equality.ma".
 
 definition antisymmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
-\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to (eq A x y).
+\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to x=y.