]> 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 d064ef619fc6918452ebbc5ce935caeb36a1c027..366c0e264fe0d201fe071d6cf4b6fad8bf7f8fa0 100644 (file)
@@ -222,10 +222,11 @@ let pp_default what uris =
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
 let pp_coercion uri do_composites arity =
-   sprintf "coercion \"%s\" %d (* %s *)" (UriManager.string_of_uri uri) arity
+   sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) 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"