X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;fp=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;h=ce4a585b3e609d52b510af84c0632e74c1356453;hb=dbb9f64a437b4abda0b9f47a527ab6135d596e28;hp=7687bc5222235543bd6da28bd876f6253710b54f;hpb=024819eeb7fcd370114ceb3dffc7907db92ab640;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 7687bc522..ce4a585b3 100644
--- 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 *)