ocaml 3.09 transition

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pc3_gen_context.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
index 4e26ce7eadad5553ce5ec1937cef2318b8ef53d8..42f03f2ab3377bdade49d49fdafad5f719b31e15 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
@@ -15,8 +15,8 @@ Require pc3_props.
                              (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
                              (x2:?) (subst1 d u t2 (lift (1) d x2)) ->
                              (pc3 a x1 x2).
-      Intros; Pc3Confluence; Repeat Pr3GenContext.
-      Subst1Confluence; Rewrite H in H3; Clear H x3; XEAuto.
+      Intros; Pc3Unfold; Repeat Pr3GenContext.
+      Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.
       Qed.
 
    End pc3_gen_context.