New argument for LApply: the ident for the generated hypothesis.

[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..0bb6b3222c5bd6460250bbde036a8778adf0ff9a 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)