]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
* new binary matitatop
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index bc4346e91c7b29646da92164e72b6fa25e865fdd..ee099e4202a4539e97bfa3baa975c57e9f804051 100644 (file)
@@ -220,6 +220,7 @@ let pp_obj = function
 
 let pp_command = function
   | Qed _ -> "qed"
+  | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
   | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
   | Alias (_,s) -> pp_alias s