]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
Fixing universe levels for saturations and (partially) basic_topologies.
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 9d8d41537fdcbbb198c67a3b031c278a06a82b40..0399e4ca3c9a00bac560a5c822b376a898d3496d 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
+  | UnificationHint (_,t) -> 
+      "unification hint " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""