]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v
ocaml 3.09 transition
[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pr3_subst1.v
index 78c9834d5df71093c8aa88f373cd0a155a7fe8fa..3db6ce0005954420aa8c260912cd87df123d338b 100644 (file)
@@ -30,4 +30,3 @@ Require pr3_defs.
                LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
                XElim H1; Intros
             | _ -> Pr2Subst1.
-