X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr3_gen_context.v;h=a7f3e92bebd17b9854326e7cbd58d03e073b03b6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f0662babeb3da93ec01dcbcce4eaa47fcd0118b7;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v
index f0662babe..a7f3e92be 100644
--- 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 ].