better message

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 0ef9ec617f2ba7a0ea3e9f1a9b689e5aaba735ab..352c925fbba057947ede41bab2f91fec9f6aa929 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -408,8 +408,9 @@ EXTEND
         let idents = match ident with None -> [] | Some id -> [id] in
         TacticAst.Intros (loc, Some 1, idents)
     | IDENT "lapply"; what = tactic_term; 
-      to_what = OPT [ "to" ; t = tactic_term -> t ] ->
-        TacticAst.LApply (loc, to_what, what)
+      to_what = OPT [ "to" ; t = tactic_term -> t ];
+      ident = OPT [ "using" ; id = IDENT -> id ] ->
+        TacticAst.LApply (loc, to_what, what, ident)
     | IDENT "left" -> TacticAst.Left loc
     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
@@ -569,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 ] ->