Syntactic change:

[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..40157d849f9baf53e9f871f07ef5432adba152c9 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.