From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Jun 2005 13:45:59 +0000 (+0000)
Subject: New argument (the identifier) to generalize.
X-Git-Tag: INDEXING_NO_PROOFS~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c91796631682cba2972b964c7570c3437ccd971f;p=helm.git

New argument (the identifier) to generalize.
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index efacfccd7..3fdda212d 100644
--- 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 8b66ca0e6..47f275a68 100644
--- 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 bbb2c935b..019ba6172 100644
--- 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