New argument (the identifier) to generalize.

[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 efacfccd762d6ef8102c503e3761587924f417a2..3fdda212d83339aac2c681bbdcc573eac5361e66 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -384,9 +384,11 @@ EXTEND
         TacticAst.Fourier loc
     | IDENT "fwd"; t = term ->
         TacticAst.FwdSimpl (loc, t)
-    | IDENT "generalize"; t = tactic_term; p = OPT [ pattern_spec ] ->
+    | IDENT "generalize"; t = tactic_term;
+       id = OPT [ "as" ; id = IDENT -> id ];
+       p = OPT [ pattern_spec ] ->
        let p = match p with None -> [], None | Some p -> p in
-       TacticAst.Generalize (loc,t,p)
+       TacticAst.Generalize (loc,t,id,p)
     | IDENT "goal"; n = NUM ->
         TacticAst.Goal (loc, int_of_string n)
     | IDENT "injection"; t = term ->