X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr3_subst1.v;h=3db6ce0005954420aa8c260912cd87df123d338b;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=78c9834d5df71093c8aa88f373cd0a155a7fe8fa;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;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.
-