moved coercion to library (work in progress)

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

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 36b54694d4092ea450806a4cd0de459c61995716..28f42ca6d5eb4e7f1bc7a234598aa5138ca44919 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -218,7 +218,8 @@ let pp_command = function
   | 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) ->
@@ -286,7 +287,8 @@ 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 _