abstracted pretty printers over inner pretty printing units (terms, lazy terms, and...

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

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index 3d176fbe5190d721f0728c85f7b7c3b28ddbbec0..e1ae5865d43e6ef1dcc0e2de060b46e9636f06e3 100644 (file)
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -28,7 +28,7 @@ type direction = [ `LeftToRight | `RightToLeft ]
 type loc = CicNotationPt.location
 
 type ('term, 'lazy_term, 'ident) pattern =
-  'lazy_term option * ('ident * 'term) list * 'term
+  'lazy_term option * ('ident * 'term) list * 'term option
 
 type ('term, 'ident) type_spec =
    | Ident of 'ident
@@ -114,9 +114,9 @@ type alias_spec =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 4
+let magic = 5
 
-type ('term,'obj) command =
+type 'obj command =
   | Default of loc * string * UriManager.uri list
   | Include of loc * string
   | Set of loc * string * string
@@ -125,7 +125,7 @@ type ('term,'obj) command =
       (** name.
        * Name is needed when theorem was started without providing a name
        *)
-  | Coercion of loc * 'term * bool (* add composites *)
+  | Coercion of loc * UriManager.uri * bool (* add composites *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
@@ -175,7 +175,7 @@ let is_punctuation =
   | _ -> false
 
 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
-  | Command of loc * ('term,'obj) command
+  | Command of loc * 'obj command
   | Macro of loc * 'term macro 
   | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
       * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)