1. matitaEngine splitted into disambiguation (now in grafite_parser) and

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

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index f3687789b4ffef162f9c341c14fae13008529b9a..a7b0f3eea365541a15647a4e1919453702abfe13 100644 (file)
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -23,11 +23,9 @@
  * http://helm.cs.unibo.it/
  *)
 
-module Ast = CicNotationPt
-
 type direction = [ `LeftToRight | `RightToLeft ]
 
-type loc = Ast.location
+type loc = CicNotationPt.location
 
 type ('term, 'lazy_term, 'ident) pattern =
   'lazy_term option * ('ident * 'term) list * 'term
@@ -36,11 +34,11 @@ type ('term, 'ident) type_spec =
    | Ident of 'ident
    | Type of UriManager.uri * int 
 
-type reduction =
+type 'lazy_term reduction =
   [ `Normalize
   | `Reduce
   | `Simpl
-  | `Unfold of CicNotationPt.term option
+  | `Unfold of 'lazy_term option
   | `Whd ]
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
@@ -124,7 +122,7 @@ let eq_metadata = (=)
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 3
+let magic = 4
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
@@ -139,12 +137,12 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
-      int * Ast.term
+  | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
+      int * CicNotationPt.term
       (* direction, l1 pattern, associativity, precedence, l2 pattern *)
   | Interpretation of loc *
-      string * (string * Ast.argument_pattern list) *
-        Ast.cic_appl_pattern
+      string * (string * CicNotationPt.argument_pattern list) *
+        CicNotationPt.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
   | Metadata of loc * metadata