integration with paramodulation

[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 7d09e2d6a5933c53c59035d6be3764a219205987..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
@@ -133,7 +137,7 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
+  | Notation of loc * CicNotationPt.term * Gramext.g_assoc * int *
       CicNotationPt.term
       (* level 1 pattern, associativity, precedence, level 2 pattern *)
   | Interpretation of loc *