1. metadata are no longer stored in .moo files.

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

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 7687bc5222235543bd6da28bd876f6253710b54f..ce4a585b3e609d52b510af84c0632e74c1356453 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -206,11 +206,6 @@ 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"
@@ -235,7 +230,6 @@ 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 *)
 
@@ -293,7 +287,6 @@ let pp_cic_command = function
   | Render _
   | Dump _
   | Interpretation _
-  | Metadata _
   | Notation _
   | Obj _ -> assert false (* not implemented *)