some reorganization and some corrections

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
index 157cb74561c09fe1811bce21327ae4cef7100c8a..37d8de88d4c0000fcde46f0eb60e6ddfc9cda2e4 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
@@ -13,11 +13,16 @@ Require Export Base.
                       |  Flat : F -> K.
 
       Inductive Set T := TSort : nat -> T
-                      |  TBRef : nat -> T
+                      |  TLRef : nat -> T
                       |  TTail : K -> T -> T -> T.
 
       Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
 
+      Tactic Definition TGenBase :=
+         Match Context With
+            | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
+           | _                                         -> Idtac.
+
       Definition s: K -> nat -> nat := [k;i] Cases k of
          | (Bind _) => (S i)
          | (Flat _) => i