ocaml 3.09 transition

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

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 2848c08c5753086d5ffb5e9073c1b2687ee95bae..4cbea3529a7ec983b39f814f1243f1a5f92568ab 100644 (file)
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -65,8 +65,7 @@ theorem Or_ind':
     \forall p:A \lor B. P p.
  intros.
  apply
-  ([\lambda p.P p]
-   match p with
+  (match p return \lambda p.P p with
     [(or_introl p) \Rightarrow H p
     |(or_intror q) \Rightarrow H1 q]).
 qed.