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

diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli
index 41b775562d43557a151a96ecc07bf962bd2e33c0..9eb98c1d3339ad2ef3142bc30fd7b12196c126d5 100644 (file)
--- a/helm/ocaml/grafite/cicNotation.mli
+++ b/helm/ocaml/grafite/cicNotation.mli
@@ -26,7 +26,7 @@
 type notation_id
 
 val process_notation:
-  ('a, 'b) GrafiteAst.command -> ('a, 'b) GrafiteAst.command * notation_id list
+  'obj GrafiteAst.command -> 'obj GrafiteAst.command * notation_id list
 
 val remove_notation: notation_id -> unit
 

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 *)

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index dac1d6e051e6e81b05cf9eda4b5e038ddea3b410..617a6d5637abcc3b1111d8f0a7d089bdf47165ab 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -31,32 +31,29 @@ let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
 
-let pp_term_ast term = CicNotationPp.pp_term term
-let pp_term_cic term = CicPp.ppterm term
-
 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
-let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
-
-let pp_reduction_kind = function
+let pp_reduction_kind ~term_pp = function
   | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
-  | `Unfold (Some t) -> "unfold " ^ pp_term_ast t
+  | `Unfold (Some t) -> "unfold " ^ term_pp t
   | `Unfold None -> "unfold"
   | `Whd -> "whd"
  
-  
-let pp_pattern (t, hyp, goal) = 
-  let pp_hyp_pattern l =
-    String.concat "; "
-      (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in
-  let pp_t t =
-   match t with
-      None -> ""
-    | Some t -> pp_term_ast t
-  in
-   pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
+let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = 
+  let what_text =
+    match what with
+    | None -> ""
+    | Some t -> sprintf "in match (%s) " (lazy_term_pp t) in
+  let hyp_text =
+    String.concat " "
+      (List.map (fun (name, p) -> sprintf "%s:(%s)" name (term_pp p)) hyp) in
+  let goal_text =
+    match goal with
+    | None -> ""
+    | Some t -> sprintf "\\vdash (%s)" (term_pp t) in
+  sprintf "%sin %s%s" what_text hyp_text goal_text
 
 let pp_intros_specs = function
    | None, []         -> ""
@@ -64,20 +61,25 @@ let pp_intros_specs = function
    | None, idents     -> Printf.sprintf " names %s" (pp_idents idents)
    | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents)
 
-let rec pp_tactic = function
-  | Absurd (_, term) -> "absurd" ^ pp_term_ast term
-  | Apply (_, term) -> "apply " ^ pp_term_ast term
+let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
+
+let rec pp_tactic ~term_pp ~lazy_term_pp =
+  let pp_reduction_kind = pp_reduction_kind ~term_pp in
+  let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
+  function
+  | Absurd (_, term) -> "absurd" ^ term_pp term
+  | Apply (_, term) -> "apply " ^ term_pp term
   | Auto _ -> "auto"
   | Assumption _ -> "assumption"
   | Change (_, where, with_what) ->
-      sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what)
+      sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,id) -> sprintf "clear %s" id
   | ClearBody (_,id) -> sprintf "clearbody %s" id
-  | Compare (_,term) -> "compare " ^ pp_term_ast term
+  | Compare (_,term) -> "compare " ^ term_pp term
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
   | Cut (_, ident, term) ->
-     "cut " ^ pp_term_ast term ^
+     "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | DecideEquality _ -> "decide equality"
   | Decompose (_, [], what, names) ->
@@ -89,31 +91,31 @@ let rec pp_tactic = function
       in
       let types = List.rev_map to_ident types in
       sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) 
-  | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
+  | Discriminate (_, term) -> "discriminate " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
-      sprintf "elim " ^ pp_term_ast term ^
-      (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+      sprintf "elim " ^ term_pp term ^
+      (match using with None -> "" | Some term -> " using " ^ term_pp term)
       ^ pp_intros_specs (num, idents) 
   | ElimType (_, term, using, num, idents) ->
-      sprintf "elim type " ^ pp_term_ast term ^
-      (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+      sprintf "elim type " ^ term_pp term ^
+      (match using with None -> "" | Some term -> " using " ^ term_pp term)
       ^ pp_intros_specs (num, idents)
-  | Exact (_, term) -> "exact " ^ pp_term_ast term
+  | Exact (_, term) -> "exact " ^ term_pp term
   | Exists _ -> "exists"
   | Fold (_, kind, term, pattern) ->
       sprintf "fold %s %s %s" (pp_reduction_kind kind)
-       (pp_term_ast term) (pp_pattern pattern)
+       (lazy_term_pp term) (pp_tactic_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
   | Generalize (_, pattern, ident) ->
-     sprintf "generalize %s%s" (pp_pattern pattern)
+     sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fail _ -> "fail"
   | Fourier _ -> "fourier"
   | IdTac _ -> "id"
-  | Injection (_, term) -> "injection " ^ pp_term_ast term
+  | Injection (_, term) -> "injection " ^ term_pp term
   | Intros (_, None, []) -> "intro"
   | Intros (_, num, idents) ->
       sprintf "intros%s%s"
@@ -122,26 +124,26 @@ let rec pp_tactic = function
   | LApply (_, level_opt, terms, term, ident_opt) -> 
       sprintf "lapply %s%s%s%s" 
         (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
-        (pp_term_ast term) 
-        (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms)
+        (term_pp term) 
+        (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
         (match ident_opt with None -> "" | Some ident -> " using " ^ ident)
   | Left _ -> "left"
-  | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
+  | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident
   | Reduce (_, kind, pat) ->
-      sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat)
+      sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
   | Reflexivity _ -> "reflexivity"
   | Replace (_, pattern, t) ->
-      sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t)
+      sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
   | Rewrite (_, pos, t, pattern) -> 
       sprintf "rewrite %s %s %s" 
         (if pos = `LeftToRight then ">" else "<")
-        (pp_term_ast t)
-        (pp_pattern pattern)
+        (term_pp t)
+        (pp_tactic_pattern pattern)
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
-  | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
+  | Transitivity (_, term) -> "transitivity " ^ term_pp term
 
 let pp_search_kind = function
   | `Locate -> "locate"
@@ -150,31 +152,23 @@ let pp_search_kind = function
   | `Elim -> "elim"
   | `Instance -> "instance"
 
-let pp_macro pp_term = function 
+let pp_macro ~term_pp = function 
   (* Whelp *)
-  | WInstance (_, term) -> "whelp instance " ^ pp_term term
-  | WHint (_, t) -> "whelp hint " ^ pp_term t
+  | WInstance (_, term) -> "whelp instance " ^ term_pp term
+  | WHint (_, t) -> "whelp hint " ^ term_pp t
   | WLocate (_, s) -> "whelp locate " ^ s
-  | WElim (_, t) -> "whelp elim " ^ pp_term t
-  | WMatch (_, term) -> "whelp match " ^ pp_term term
+  | WElim (_, t) -> "whelp elim " ^ term_pp t
+  | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
-(*   | Abort _ -> "Abort" *)
-  | Check (_, term) -> sprintf "Check %s" (pp_term term)
+  | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-(*   | Redo (_, None) -> "Redo"
-  | Redo (_, Some n) -> sprintf "Redo %d" n *)
   | Search_pat (_, kind, pat) ->
       sprintf "search %s \"%s\"" (pp_search_kind kind) pat
   | Search_term (_, kind, term) ->
-      sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
-(*   | Undo (_, None) -> "Undo"
-  | Undo (_, Some n) -> sprintf "Undo %d" n *)
+      sprintf "search %s %s" (pp_search_kind kind) (term_pp term)
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
 
-let pp_macro_ast = pp_macro pp_term_ast
-let pp_macro_cic = pp_macro pp_term_cic
-
 let pp_alias = function
   | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
   | Symbol_alias (symb, instance, desc) ->
@@ -224,23 +218,18 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
     (pp_precedence prec)
     (pp_l2_pattern l2_pattern)
     
-let pp_coercion_ast term do_composites =
-   sprintf "coercion %s (* %s *)" (pp_term_ast term) 
-     (if do_composites then "compounds" else "no compounds")
-
-let pp_coercion_cic term do_composites =
-   sprintf "coercion %s (* %s *)" (pp_term_cic term) 
+let pp_coercion uri do_composites =
+   sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
      (if do_composites then "compounds" else "no compounds")
     
-let pp_command = function
+let pp_command ~obj_pp = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_,term, do_composites) ->
-      pp_coercion_ast term do_composites
+  | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
   | Alias (_,s) -> pp_alias s
-  | Obj (_,obj) -> CicNotationPp.pp_obj obj
+  | Obj (_,obj) -> obj_pp obj
   | Default (_,what,uris) ->
       pp_default what uris
   | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
@@ -250,15 +239,20 @@ let pp_command = function
   | Render _
   | Dump _ -> assert false  (* ZACK: debugging *)
 
-let rec pp_tactical = function
+let rec pp_tactical ~term_pp ~lazy_term_pp =
+  let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
+  let pp_tacticals = pp_tacticals ~lazy_term_pp ~term_pp in
+  function
   | Tactic (_, tac) -> pp_tactic tac
-  | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
-  | Repeat (_, tac) -> "repeat " ^ pp_tactical tac
+  | Do (_, count, tac) ->
+      sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac)
+  | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac
   | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
   | Then (_, tac, tacs) ->
-      sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
+      sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac)
+        (pp_tacticals ~sep:" | " tacs)
   | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
-  | Try (_, tac) -> "try " ^ pp_tactical tac
+  | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
   | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
 
   | Dot _ -> "."
@@ -272,46 +266,29 @@ let rec pp_tactical = function
   | Unfocus _ -> "unfocus"
   | Skip _ -> "skip"
 
-and pp_tacticals ~sep tacs = String.concat sep (List.map pp_tactical tacs)
-
-let pp_tactical tac = pp_tactical tac
-let pp_tactic tac = pp_tactic tac 
-let pp_command tac = pp_command tac
+and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs =
+  String.concat sep (List.map (pp_tactical~lazy_term_pp ~term_pp) tacs)
 
-let pp_executable = function
-  | Macro (_,x) -> pp_macro_ast x
-  | Tactical (_, tac, Some punct) -> pp_tactical tac ^ pp_tactical punct
-  | Tactical (_, tac, None) -> pp_tactical tac
-  | Command (_,x) -> pp_command x
+let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
+  function
+  | Macro (_, macro) -> pp_macro ~term_pp macro
+  | Tactical (_, tac, Some punct) ->
+      pp_tactical ~lazy_term_pp ~term_pp tac
+      ^ pp_tactical ~lazy_term_pp ~term_pp punct
+  | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
+  | Command (_, cmd) -> pp_command ~obj_pp cmd
                       
-let pp_comment = function
+let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
+  function
   | Note (_,str) -> sprintf "(* %s *)" str
-  | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
-
-let pp_statement = function
-  | Executable (_, ex) -> pp_executable ex
-  | Comment (_, c) -> pp_comment c
-
+  | Code (_,code) ->
+      sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
 
+let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
+  function
+  | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex
+  | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c
   
-let pp_cic_command = function
-  | Include (_,path) -> "include " ^ path
-  | Qed _ -> "qed"
-  | Drop _ -> "drop"
-  | Coercion (_,term, do_composites) ->
-      pp_coercion_cic term do_composites
-  | Obj (_,obj) -> CicPp.ppobj obj
-  | Set _-> assert false (* not implemented *)
-  | Alias (_, alias) -> pp_alias alias
-  | Default (_,what,uris) ->
-      pp_default what uris
-  | Render _ -> assert false (* not implemented *)
-  | Dump _ -> assert false (* not implemented *)
-  | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
-      pp_interpretation dsc symbol arg_patterns cic_appl_pattern
-  | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
-      pp_notation dir_opt l1_pattern assoc prec l2_pattern
-
 let pp_dependency = function
   | IncludeDep str -> "include \"" ^ str ^ "\""
   | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""

diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli
index 1ecfb4352a4063fa7a2687cc57711c35c242c7e4..80d2174f70dff3512fc96b73dba4b5e475166a7d 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.mli
+++ b/helm/ocaml/grafite/grafiteAstPp.mli
@@ -24,43 +24,56 @@
  *)
 
 val pp_tactic:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
   GrafiteAst.tactic ->
     string
 
-val pp_command:
-  (CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command -> string
-val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
+val pp_tactic_pattern:
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  ('term, 'lazy_term, string) GrafiteAst.pattern ->
+    string
+
+val pp_reduction_kind:
+  term_pp:('a -> string) ->
+  'a GrafiteAst.reduction ->
+    string
+
+val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string
+val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string
+val pp_alias: GrafiteAst.alias_spec -> string
+val pp_dependency:  GrafiteAst.dependency -> string
 
 val pp_comment:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  obj_pp:('obj -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
   GrafiteAst.comment ->
     string
 
 val pp_executable:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  obj_pp:('obj -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
   GrafiteAst.code ->
     string
 
 val pp_statement:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  obj_pp:('obj -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
   GrafiteAst.statement ->
     string
 
-val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string
-val pp_macro_cic: Cic.term GrafiteAst.macro -> string
-
 val pp_tactical:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
   GrafiteAst.tactical ->
     string
 
-val pp_alias: GrafiteAst.alias_spec -> string
-
-val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string
-
-val pp_dependency:  GrafiteAst.dependency -> string
-

diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index 8b4f8858b8bf8f3b33b0b50f0670c1499d370d80..8c6928b7b6423b41e217c70074bd49322721ffd1 100644 (file)
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -27,7 +27,7 @@ exception Checksum_failure of string
 exception Corrupt_moo of string
 exception Version_mismatch of string
 
-type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
+type ast_command = Cic.obj GrafiteAst.command
 type moo = ast_command list
 
 let marshal_flags = []
@@ -50,13 +50,14 @@ let rehash_cmd_uris =
       in
       let appl_pattern = aux cic_appl_pattern in
       GrafiteAst.Interpretation (loc, dsc, args, appl_pattern)
-  | GrafiteAst.Coercion (loc, term, close) ->
-      GrafiteAst.Coercion (loc, CicUtil.rehash_term term, close)
+  | GrafiteAst.Coercion (loc, uri, close) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close)
   | GrafiteAst.Notation _
   | GrafiteAst.Alias _ as cmd -> cmd
   | cmd ->
       prerr_endline "Found a command not expected in a .moo:";
-      prerr_endline (GrafiteAstPp.pp_cic_command cmd);
+      let obj_pp _ = assert false in
+      prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd);
       assert false
 
 (** .moo file format

diff --git a/helm/ocaml/grafite/grafiteMarshal.mli b/helm/ocaml/grafite/grafiteMarshal.mli
index 9be797a44fb6e76ba389e37f3db31c4d55e65fec..4b49cfc41d771f095713ea0962ea6b6026bb1252 100644 (file)
--- a/helm/ocaml/grafite/grafiteMarshal.mli
+++ b/helm/ocaml/grafite/grafiteMarshal.mli
@@ -28,7 +28,7 @@ exception Checksum_failure of string
 exception Corrupt_moo of string
 exception Version_mismatch of string
 
-type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
+type ast_command = Cic.obj GrafiteAst.command
 type moo = ast_command list
 
 val save_moo: fname:string -> moo -> unit