added Drop

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 0bb6b3222c5bd6460250bbde036a8778adf0ff9a..352c925fbba057947ede41bab2f91fec9f6aa929 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -570,8 +570,9 @@ EXTEND
   ];
   
   command: [[
-      [ IDENT "set"    ]; n = QSTRING; v = QSTRING ->
+       [ IDENT "set" ]; n = QSTRING; v = QSTRING ->
         TacticAst.Set (loc, n, v)
+    |  [ IDENT "drop" ] -> TacticAst.Drop loc
     | [ IDENT "qed"   ] -> TacticAst.Qed loc
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->