New argument (the hypothesis name) for cut.

[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 1b67821c1ec8630a3d24dd71c7ae4c3e3e2042da..efacfccd762d6ef8102c503e3761587924f417a2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -361,8 +361,8 @@ EXTEND
         TacticAst.Constructor (loc,int_of_string n)
     | IDENT "contradiction" ->
         TacticAst.Contradiction loc
-    | IDENT "cut"; t = tactic_term ->
-        TacticAst.Cut (loc, t)
+    | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
+        TacticAst.Cut (loc, ident, t)
     | IDENT "decide"; IDENT "equality" ->
         TacticAst.DecideEquality loc
     | IDENT "decompose"; where = term ->