X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;h=ce4a585b3e609d52b510af84c0632e74c1356453;hb=6a388079100673e4f71d28a8a53ea029ee1b08df;hp=36b54694d4092ea450806a4cd0de459c61995716;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 36b54694d..ce4a585b3 100644
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -27,8 +27,6 @@ open Printf
 
 open GrafiteAst
 
-module Ast = CicNotationPt
-
 let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
@@ -186,7 +184,7 @@ let pp_alias = function
       sprintf "alias num (instance %d) = \"%s\"" instance desc
   
 let pp_argument_pattern = function
-  | Ast.IdentArg (eta_depth, name) ->
+  | CicNotationPt.IdentArg (eta_depth, name) ->
       let eta_buf = Buffer.create 5 in
       for i = 1 to eta_depth do
         Buffer.add_string eta_buf "\\eta."
@@ -208,17 +206,13 @@ 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"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term)
+  | Coercion (_,term, _do_composites) ->
+     sprintf "coercion %s" (pp_term_ast term)
   | Alias (_,s) -> pp_alias s
   | Obj (_,obj) -> CicNotationPp.pp_obj obj
   | Default (_,what,uris) ->
@@ -236,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 *)
 
@@ -286,14 +279,14 @@ let pp_cic_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
-  | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term)
+  | Coercion (_,term,_add_composites) ->
+     sprintf "coercion %s" (CicPp.ppterm term)
   | Set _
   | Alias _
   | Default _
   | Render _
   | Dump _
   | Interpretation _
-  | Metadata _
   | Notation _
   | Obj _ -> assert false (* not implemented *)