EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
| TacticAst.FwdSimpl (_, term) ->
Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
- | TacticAst.LApply (_, term) ->
- let f (name, term) = Cic.Name name, term in
- Tactics.lapply term
+ | TacticAst.LApply (_, to_what, what) ->
+ Tactics.lapply ?to_what what
let eval_tactical status tac =
let apply_tactic tactic =
| TacticAst.FwdSimpl (loc, term) ->
let status, term = disambiguate_term status term in
status, TacticAst.FwdSimpl (loc, term)
- | TacticAst.LApply (loc, term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.LApply (loc, term)
+ | TacticAst.LApply (loc, Some to_what, what) ->
+ let status, to_what = disambiguate_term status to_what in
+ let status, what = disambiguate_term status what in
+ status, TacticAst.LApply (loc, Some to_what, what)
+ | TacticAst.LApply (loc, None, what) ->
+ let status, what = disambiguate_term status what in
+ status, TacticAst.LApply (loc, None, what)
let rec disambiguate_tactical status = function
| TacticAst.Tactic (loc, tactic) ->