ocaml 3.09 transition

[helm.git] / helm / matita / library / logic / equality.ma

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 7e67c056ca9a9f74bd503fe752d904781e437200..b87dc6c95656dcf5de3c3ceb00e9ed105067c6b8 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -32,8 +32,7 @@ theorem eq_ind':
   P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
  intros.
  exact
-  ([\lambda y. \lambda p.P y p]
-   match p with
+  (match p return \lambda y. \lambda p.P y p with
     [refl_eq \Rightarrow H]).
 qed.
  
@@ -42,14 +41,14 @@ simplify.intros.apply refl_eq.
 qed.
     
 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
-simplify.intros.elim H. apply refl_eq.
+unfold symmetric.intros.elim H. apply refl_eq.
 qed.
 
 theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).
-simplify.intros.elim H1.assumption.
+unfold transitive.intros.elim H1.assumption.
 qed.
 
 theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z