| TacticAst.Exact (_, term) -> Tactics.exact term
| TacticAst.Exists _ -> Tactics.exists
| TacticAst.Fail _ -> Tactics.fail
- | TacticAst.Fold (_, reduction_kind, pattern) ->
+ | TacticAst.Fold (_, reduction_kind, term, pattern) ->
let reduction =
match reduction_kind with
| `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
| `Simpl -> ProofEngineReduction.simpl
| `Whd -> CicReduction.whd ~delta:false ~subst:[]
in
- Tactics.fold ~reduction ~pattern
+ Tactics.fold ~reduction ~term ~pattern
| TacticAst.Fourier _ -> Tactics.fourier
- | TacticAst.FwdSimpl (_, term) ->
- Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
+ | TacticAst.FwdSimpl (_, hyp, names) ->
+ Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
| TacticAst.Generalize (_,pattern,ident) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
| TacticAst.Intros (_, Some num, names) ->
PrimitiveTactics.intros_tac ~howmany:num
~mk_fresh_name_callback:(namer_of names) ()
- | TacticAst.LApply (_, to_what, what, ident) ->
+ | TacticAst.LApply (_, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?to_what what
+ Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
| TacticAst.Left _ -> Tactics.left
| TacticAst.LetIn (loc,term,name) ->
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
status, TacticAst.ElimType (loc, cic)
| TacticAst.Exists loc -> status, TacticAst.Exists loc
| TacticAst.Fail loc -> status,TacticAst.Fail loc
- | TacticAst.Fold (loc,reduction_kind, pattern) ->
+ | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Fold (loc,reduction_kind, pattern)
- | TacticAst.FwdSimpl (loc, term) ->
let status, term = disambiguate_term status term in
- status, TacticAst.FwdSimpl (loc, term)
+ status, TacticAst.Fold (loc,reduction_kind, term, pattern)
+ | TacticAst.FwdSimpl (loc, hyp, names) ->
+ status, TacticAst.FwdSimpl (loc, hyp, names)
| TacticAst.Fourier loc -> status, TacticAst.Fourier loc
| TacticAst.Generalize (loc,pattern,ident) ->
let status, pattern = disambiguate_pattern status pattern in
status, TacticAst.Injection (loc,term)
| TacticAst.Intros (loc, num, names) ->
status, TacticAst.Intros (loc, num, names)
- | TacticAst.LApply (loc, to_what, what, ident) ->
- let status, to_what =
- match to_what with
- None -> status,None
- | Some to_what ->
- let status, to_what = disambiguate_term status to_what in
- status, Some to_what
+ | TacticAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term (status, to_what) =
+ let status, term = disambiguate_term status term in
+ status, term :: to_what
in
+ let status, to_what = List.fold_right f to_what (status, []) in
let status, what = disambiguate_term status what in
- status, TacticAst.LApply (loc, to_what, what, ident)
+ status, TacticAst.LApply (loc, depth, to_what, what, ident)
| TacticAst.Left loc -> status, TacticAst.Left loc
| TacticAst.LetIn (loc, term, name) ->
let status, term = disambiguate_term status term in