let eval_ng_tac (text, prefix_len, tac) =
match tac with
| GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
- | GrafiteAst.NId _ -> fun x -> x
+ | GrafiteAst.NCases (_loc, what, where) ->
+ NTactics.cases_tac
+ ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
+ | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
+ | GrafiteAst.NChange (_loc, pat, ww) ->
+ NTactics.change_tac
+ ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww)
+ | GrafiteAst.NElim (_loc, what, where) ->
+ NTactics.elim_tac
+ ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
+ | GrafiteAst.NEval (_loc, where, reduction) ->
+ NTactics.eval_tac ~reduction ~where:(text,prefix_len,where)
+ | GrafiteAst.NGeneralize (_loc, where) ->
+ NTactics.generalize_tac ~where:(text,prefix_len,where)
+ | GrafiteAst.NId _ -> (fun x -> x)
+ | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+ | GrafiteAst.NLetIn (_loc,where,what,name) ->
+ NTactics.letin_tac ~where:(text,prefix_len,where)
+ ~what:(text,prefix_len,what) name
+ | GrafiteAst.NRewrite (_loc,dir,what,where) ->
+ NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
;;
let rec eval_command = {ec_go = fun ~disambiguate_command opts status
prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
{ status with
GrafiteTypes.ng_status =
- GrafiteTypes.ProofMode { NTactics.gstatus = ninitial_stack;
+ GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack;
istatus = {
- NTactics.pstatus =
+ NTacStatus.pstatus =
NUri.uri_of_string suri, 0, nmenv, nsubst,
(NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
lstatus = nlexicon_status} }
| GrafiteTypes.ProofMode nstatus ->
let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
- NTactics.pp_tac_status nstatus;
+ NTacStatus.pp_tac_status nstatus;
{ status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
| GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =