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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
index ec1f9e758..63373a401 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
@@ -7,6 +7,11 @@ Require Export terms_defs.
 
       Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
 
+      Tactic Definition CGenBase :=
+         Match Context With
+            | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
+	    | _                                         -> TGenBase.
+
       Definition r: K -> nat -> nat := [k;i] Cases k of
          | (Bind _) => i
          | (Flat _) => (S i)