ocaml 3.09 transition

[helm.git] / helm / matita / library / Z / orders.ma

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 186533ea08fb45ae82fd590c8e52f7ffded634c4..c39f693085398eedf4a95a9f15898f05e6cee264 100644 (file)
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -71,9 +71,9 @@ theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with (\forall x:Z. x < x \to False).
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 cut (pos n < pos n \to False).
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 qed.
 
 theorem irrefl_Zlt: irreflexive Z Zlt