X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=ee099e4202a4539e97bfa3baa975c57e9f804051;hb=94c9255e1f3095440f4d49ea1d75443a5a343185;hp=bc4346e91c7b29646da92164e72b6fa25e865fdd;hpb=e74526f044f57e77e99c777b5f9354fdd2c74a74;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bc4346e91..ee099e420 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -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