X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=191323599638b3937ec47bd79adf7a07e58c2b5c;hb=94c9255e1f3095440f4d49ea1d75443a5a343185;hp=1525cfd8b7f132315dffbf3c8c4a4e5672924d08;hpb=e74526f044f57e77e99c777b5f9354fdd2c74a74;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 1525cfd8b..191323599 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -128,6 +128,7 @@ type obj =
 
 type ('term,'obj) command =
   | Set of loc * string * string
+  | Drop of loc
   | Qed of loc
       (** name.
        * Name is needed when theorem was started without providing a name