merged cic_notation with disambiguation: good luck!

[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 5117fd493e89579d2ac3a330e563c1938858c453..e845e575557cf9c0a86cf13b82baf3a2d60697dc 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -120,14 +120,6 @@ type obj =
      (string * CicNotationPt.term) list * string * CicNotationPt.term *
       (string * CicNotationPt.term) list
 
-type argument_pattern =
-  | IdentArg of int * string (* eta-depth, name *)
-
-type cic_appl_pattern =
-  | UriPattern of UriManager.uri
-  | VarPattern of string
-  | ApplPattern of cic_appl_pattern list
-
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
   | Include of loc * string
@@ -141,9 +133,13 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term
+  | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
+      CicNotationPt.term
       (* level 1 pattern, associativity, precedence, level 2 pattern *)
-  | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern
+  | Interpretation of loc *
+      string * (string * CicNotationPt.argument_pattern list) *
+        CicNotationPt.cic_appl_pattern
+      (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
     (* DEBUGGING *)
   | Dump of loc (* dump grammar on stdout *)