]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
minor changes to make the library compile after wilmers new exists.
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 0399e4ca3c9a00bac560a5c822b376a898d3496d..9e3ea3b5a91bc8c6f299609d9d400c8b36a90f84 100644 (file)
@@ -313,6 +313,8 @@ let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
   | Coercion (_, t, do_composites, i, j) ->
      pp_coercion ~term_pp t do_composites i j
+  | PreferCoercion (_,t) -> 
+     "prefer coercion " ^ term_pp t
   | UnificationHint (_,t) -> 
       "unification hint " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris