]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite/grafiteAstPp.ml
Added a new command "index" for the indexing terms in the "universe".
[helm.git] / components / grafite / grafiteAstPp.ml
index 2e3d95abe6c879a93efd8419c8602adec8fb7812..366c0e264fe0d201fe071d6cf4b6fad8bf7f8fa0 100644 (file)
@@ -226,6 +226,7 @@ let pp_coercion uri do_composites arity =
      (if do_composites then "compounds" else "no compounds")
     
 let pp_command ~term_pp ~obj_pp = function
+  | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
   | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"