ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v
index f0662babeb3da93ec01dcbcce4eaa47fcd0118b7..a7f3e92bebd17b9854326e7cbd58d03e073b03b6 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v
@@ -15,9 +15,9 @@ Require pr3_defs.
                                       (pr3 a x1 x2)
                              ).
       Intros until 1; XElim H; Intros.
-(* case 1: pr3_r *)
+(* case 1: pr3_refl *)
       XEAuto.
-(* case 1: pr3_r *)
+(* case 1: pr3_refl *)
       Pr2GenContext.
       LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ].
       LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ].