X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcontexts_defs.v;h=a9a689235c8f71f8e373e4fba9b1be1a7190ed63;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=63373a401c4a07a469b7eca9f3ff684f4e93d9c6;hpb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
index 63373a401..a9a689235 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
@@ -2,13 +2,14 @@
 
 Require Export terms_defs.
 
-      Inductive Set C := CSort : nat -> C
-                      |  CTail : C -> K -> T -> C.
+      Inductive Set C := CSort: nat -> C
+                      |  CTail: C -> K -> T -> C.
 
       Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
 
       Tactic Definition CGenBase :=
          Match Context With
+            | [ H: (CSort ?) = (CSort ?) |- ? ]         -> Inversion H; Clear H
             | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
 	    | _                                         -> TGenBase.
 
@@ -63,11 +64,11 @@ Require Export terms_defs.
 
    Section app_props. (******************************************************)
 
-      Theorem app_csort : (t:?; i,n:?) (app (CSort n) i t) = t.
+      Theorem app_csort: (t:?; i,n:?) (app (CSort n) i t) = t.
       XElim i; Intros; Simpl; XAuto.
       Qed.
 
-      Theorem app_O : (c:?; t:?) (app c (0) t) = t.
+      Theorem app_O: (c:?; t:?) (app c (0) t) = t.
       XElim c; XAuto.
       Qed.