X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr3_subst1.v;h=3db6ce0005954420aa8c260912cd87df123d338b;hb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;hp=78c9834d5df71093c8aa88f373cd0a155a7fe8fa;hpb=50cfabb6b8136873a02f8fd1512f0b62f97e2639;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v
index 78c9834d5..3db6ce000 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v
@@ -30,4 +30,3 @@ Require pr3_defs.
                LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
                XElim H1; Intros
             | _ -> Pr2Subst1.
-