X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=48fbc4aa2115d9800e702ba8a1515beb7bbbc93a;hb=0d6486664169e87c0f2123f4923ab0aa3e544ebb;hp=e4f454ed61fd4cd3a0e80486470c01669b114544;hpb=18b2b2742fe8ebb3d11b32b9bb727f510df6927a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index e4f454ed6..48fbc4aa2 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -30,6 +30,10 @@ type loc = CicAst.location
 
 type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
 
+type ('term, 'ident) type_spec =
+   | Ident of 'ident
+   | Type of UriManager.uri * int 
+
 type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
@@ -43,7 +47,7 @@ type ('term, 'ident) tactic =
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
   | DecideEquality of loc
-  | Decompose of loc * 'term
+  | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
   | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list