some reorganization and some corrections

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v
index d9b302aca458e59fc3fe94d02ba0079e67616988..e2a78762416869ae88751c964c1170911ddd7dc2 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v
@@ -30,11 +30,11 @@ Require Export pc3_defs.
          | ty0_abbr : (c:?) (wf0 g c) ->
                       (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
                       (t:?) (ty0 g d u t) ->
-                      (ty0 g c (TBRef n) (lift (S n) (0) t))
+                      (ty0 g c (TLRef n) (lift (S n) (0) t))
          | ty0_abst : (c:?) (wf0 g c) ->
                       (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
                       (t:?) (ty0 g d u t) ->
-                      (ty0 g c (TBRef n) (lift (S n) (0) u))
+                      (ty0 g c (TLRef n) (lift (S n) (0) u))
          | ty0_bind : (c:?; u,t:?) (ty0 g c u t) ->
                       (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
                       (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
@@ -87,7 +87,7 @@ Require Export pc3_defs.
 (*#* #caption "generation lemma for bound reference" *)
 (*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
 
-      Theorem ty0_gen_bref: (g:?; c:?; x:?; n:?) (ty0 g c (TBRef n) x) ->
+      Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
                             (EX e u t | (pc3 c (lift (S n) (0) t) x) &
                                         (drop n (0) c (CTail e (Bind Abbr) u)) &
                                         (ty0 g e u t)
@@ -99,7 +99,7 @@ Require Export pc3_defs.
 
 (*#* #stop proof *) 
                             
-      Intros until 1; InsertEq H '(TBRef n); XElim H; Intros.
+      Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
 (* case 1 : ty0_conv *)
       LApply H2; [ Clear H2; Intros H2 | XAuto ].
       XElim H2; Intros; XElim H2; XEAuto.
@@ -218,8 +218,8 @@ Require Export pc3_defs.
          Match Context With
             | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
                LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
-            | [ H: (ty0 ?1 ?2 (TBRef ?3) ?4) |- ? ] ->
-               LApply (ty0_gen_bref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
+            | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
+               LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
                XElim H; Intros H; XElim H; Intros
             | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
                LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];