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=37d8de88d4c0000fcde46f0eb60e6ddfc9cda2e4;hpb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
index 37d8de88d..c84b1c2c7 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
@@ -2,24 +2,26 @@
 
 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
-                      |  TLRef : 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.
 
@@ -66,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).