+
+let eval_ng_punct (_text, _prefix_len, punct) =
+ match punct with
+ | GrafiteAst.Dot _ -> NTactics.dot_tac
+ | GrafiteAst.Semicolon _ -> fun x -> x
+ | GrafiteAst.Branch _ -> NTactics.branch_tac
+ | GrafiteAst.Shift _ -> NTactics.shift_tac
+ | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
+ | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac
+ | GrafiteAst.Merge _ -> NTactics.merge_tac
+;;
+
+let rec eval_ng_tac (text, prefix_len, tac) =
+ match tac with
+ | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
+ | GrafiteAst.NAssert (_loc, seqs) ->
+ NTactics.assert_tac
+ ((List.map
+ (function (hyps,concl) ->
+ List.map
+ (function
+ (id,`Decl t) -> id,`Decl (text,prefix_len,t)
+ |(id,`Def (b,t))->id,`Def((text,prefix_len,b),(text,prefix_len,t))
+ ) hyps,
+ (text,prefix_len,concl))
+ ) seqs)
+ | GrafiteAst.NAuto (_loc, (l,a)) ->
+ NTactics.auto_tac
+ ~params:(List.map (fun x -> "",0,x) l,a)
+ | GrafiteAst.NBranch _ -> NTactics.branch_tac
+ | 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.NDot _ -> NTactics.dot_tac
+ | GrafiteAst.NElim (_loc, what, where) ->
+ NTactics.elim_tac
+ ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
+ | GrafiteAst.NFocus (_,l) -> NTactics.focus_tac l
+ | 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.NMerge _ -> NTactics.merge_tac
+ | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
+ | GrafiteAst.NReduce (_loc, reduction, where) ->
+ NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
+ | GrafiteAst.NRewrite (_loc,dir,what,where) ->
+ NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
+ | GrafiteAst.NSemicolon _ -> fun x -> x
+ | GrafiteAst.NShift _ -> NTactics.shift_tac
+ | GrafiteAst.NSkip _ -> NTactics.skip_tac
+ | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
+ | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
+ | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
+ (eval_ng_tac (text, prefix_len, tac))
+ | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
+;;