added metadata "commands"

[helm.git] / helm / ocaml / cic_notation / grafiteAstPp.ml

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index 6a8e79bc10722535c8dff3df30ab016144ace9fe..9e4d632712a087da49db3e38813bbeac03d64af5 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -270,6 +270,11 @@ let pp_dir_opt = function
   | Some `LeftToRight -> "> "
   | Some `RightToLeft -> "< "
 
+let pp_metadata =
+  function
+  | Dependency buri -> sprintf "dependency %s" buri
+  | Baseuri buri -> sprintf "baseuri %s" buri
+
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
@@ -293,6 +298,7 @@ let pp_command = function
         (pp_associativity assoc)
         (pp_precedence prec)
         (pp_l2_pattern l2_pattern)
+  | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m)
   | Render _
   | Dump _ -> assert false  (* ZACK: debugging *)
 
@@ -338,6 +344,7 @@ let pp_cic_command = function
   | Render _
   | Dump _
   | Interpretation _
+  | Metadata _
   | Notation _
   | Obj _ -> assert false (* not implemented *)