+ | 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.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.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.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)
+;;
+
+let subst_metasenv_and_fix_names s =
+ let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+ let o =
+ NCicUntrusted.map_obj_kind ~skip_body:true
+ (NCicUntrusted.apply_subst subst []) o
+ in
+ { s with NTacStatus.istatus =
+ { s.NTacStatus.istatus with NTacStatus.pstatus =
+ u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}