From ea543eafaae687b248478db7bf6166dd912b5729 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 13:51:05 +0000 Subject: [PATCH] New argument (the identifier) to generalize. --- helm/matita/matitaEngine.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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 -- 2.39.2