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

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 650dbc9aa..89d168af3 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -52,7 +52,9 @@ let tactic_of_ast = function
   | TacticAst.Fourier _ -> Tactics.fourier
   | TacticAst.FwdSimpl (_, term) -> 
      Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
-  | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
+  | TacticAst.Generalize (_,term,ident,pat) ->
+     let names = match ident with None -> [] | Some id -> [id] in
+     Tactics.generalize ~term ~mk_fresh_name_callback:(namer_of names) pat
   | TacticAst.Goal (_, n) -> Tactics.set_goal n
   | TacticAst.Injection (_,term) -> Tactics.injection term
   | TacticAst.Intros (_, None, names) ->
@@ -428,10 +430,10 @@ let disambiguate_tactic status = function
      let status, term = disambiguate_term status term in
      status, TacticAst.FwdSimpl (loc, term)  
   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
-  | TacticAst.Generalize (loc,term,pattern) ->
+  | TacticAst.Generalize (loc,term,ident,pattern) ->
       let status,term = disambiguate_term status term in
       let pattern = disambiguate_pattern status.aliases pattern in
-      status, TacticAst.Generalize(loc,term,pattern)
+      status, TacticAst.Generalize(loc,term,ident,pattern)
   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
   | TacticAst.Injection (loc,term) ->
       let status, term = disambiguate_term status term in