From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Jun 2005 15:48:19 +0000 (+0000)
Subject: added Drop
X-Git-Tag: INDEXING_NO_PROOFS~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb3130d9da98e824a906175c4258b3d8ddd84dbd;p=helm.git

added Drop
---

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 ] ->