From bb3130d9da98e824a906175c4258b3d8ddd84dbd Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Jun 2005 15:48:19 +0000
Subject: [PATCH] added Drop

---
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 0bb6b3222..352c925fb 100644
--- 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 ] ->
-- 
2.39.2