| 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])
| TacticAst.Reflexivity _ -> Tactics.reflexivity
| TacticAst.Replace (_, pattern, with_what) ->
Tactics.replace ~pattern ~with_what
- | TacticAst.Rewrite (_, dir, t, pattern) ->
- if dir = `Left then
- EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
- else
- EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
+ | TacticAst.Rewrite (_, direction, t, pattern) ->
+ EqualityTactics.rewrite_tac ~direction ~pattern t
| TacticAst.Right _ -> Tactics.right
| TacticAst.Ring _ -> Tactics.ring
| TacticAst.Split _ -> Tactics.split
let eval_command status cmd =
match cmd with
- | TacticAst.Set (loc, name, value) -> set_option status name value
+ | TacticAst.Set (loc, name, value) ->
+ let value =
+ if name = "baseuri" then
+ MatitaMisc.strip_trailing_slash value
+ else
+ value
+ in
+ set_option status name value
| TacticAst.Drop loc -> raise Drop
| TacticAst.Qed loc ->
let uri, metasenv, bo, ty =
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