X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flogic%2Fconnectives.ma;h=4cbea3529a7ec983b39f814f1243f1a5f92568ab;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2848c08c5753086d5ffb5e9073c1b2687ee95bae;hpb=69dc6031c9e0574fa7a74ced74deeb7f9ec5695b;p=helm.git

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 2848c08c5..4cbea3529 100644
--- 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.