New argument (the identifier) to generalize.

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

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 8b66ca0e6c008daa3399221e971d64869c421d43..47f275a6892130a348d27005331b7169da9faec3 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -51,7 +51,7 @@ type ('term, 'ident) tactic =
   | Fold of loc * reduction_kind * 'term
   | Fourier of loc
   | FwdSimpl of loc * 'term
-  | Generalize of loc * 'term * ('term, 'ident) pattern
+  | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern
   | Goal of loc * int (* change current goal, argument is goal number 1-based *)
   | Injection of loc * 'term
   | Intros of loc * int option * 'ident list

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bbb2c935b7e8233f47a4f214ad22dcc441ae244e..019ba6172a2c413c777f737f4250c57475f8afd6 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -85,8 +85,10 @@ let rec pp_tactic = function
   | Exists _ -> "exists"
   | Fold (_, kind, term) ->
       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
-  | Generalize (_, term, pattern) ->
-     sprintf "generalize %s %s" (pp_term_ast term) (pp_pattern pattern)
+  | Generalize (_, term, ident, pattern) ->
+     sprintf "generalize %s%s %s" (pp_term_ast term)
+      (match ident with None -> "" | Some id -> " as " ^ id)
+      (pp_pattern pattern)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fourier _ -> "fourier"
   | Injection (_, term) -> "injection " ^ pp_term_ast term