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