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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
index 157cb7456..c84b1c2c7 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
@@ -2,22 +2,29 @@
 
 Require Export Base.
 
-      Inductive Set B := Abbr : B
-                      |  Abst : B
-                      |  Void : B.
+      Inductive Set B := Abbr: B
+                      |  Abst: B
+                      |  Void: B.
 
-      Inductive Set F := Appl : F
-                      |  Cast : F.
+      Inductive Set F := Appl: F
+                      |  Cast: F.
 
-      Inductive Set K := Bind : B -> K
-                      |  Flat : F -> K.
+      Inductive Set K := Bind: B -> K
+                      |  Flat: F -> K.
 
-      Inductive Set T := TSort : nat -> T
-                      |  TBRef : nat -> T
-                      |  TTail : K -> T -> T -> T.
+      Inductive Set T := TSort: 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: (TSort ?) = (TSort ?) |- ? ]         -> Inversion H; Clear H
+            | [ H: (TLRef ?) = (TLRef ?) |- ? ]         -> Inversion H; Clear H
+            | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
+	    | _                                         -> Idtac.
+
       Definition s: K -> nat -> nat := [k;i] Cases k of
          | (Bind _) => (S i)
          | (Flat _) => i
@@ -61,7 +68,7 @@ Require Export Base.
 
    End s_props.
 
-      Hints Resolve s_le s_lt s_inj.
+      Hints Resolve s_le s_lt s_inj : ltlc.
 
       Tactic Definition SRw :=
          Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).