]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite/grafiteAstPp.ml
GrafiteAst.Print (unused) removed.
[helm.git] / components / grafite / grafiteAstPp.ml
index c5bbe8f19fb2c0a940fede00c1c974e9af9afa80..55736e862e2cba8aa5ee548a823691af3f7810aa 100644 (file)
@@ -182,7 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
 
 let pp_associativity = function