the decompose tactic is now working

[helm.git] / helm / ocaml / cic_notation / grafiteAst.ml

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index a5c4db085837cddd78b5e89af32a49142ef1e067..f15417fc8ecea57bbaacea005ab3fc804007f1ec 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -30,6 +30,10 @@ type loc = CicNotationPt.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