| GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
| GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
- | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
+ | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+ | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
| GrafiteAst.NInversion (_loc, what, where) ->
NTactics.inversion_tac
~what:(text,prefix_len,what)
| _ -> obj_kind
in
let obj = uri,height,[],[],obj_kind in
+ prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
let old_status = status in
let status = NCicLibrary.add_obj status obj in
let index_obj =
let status =
if index_obj then
let status = index_obj_for_auto status obj in
- index_eq_for_auto status uri
+ (try index_eq_for_auto status uri
+ with _ -> status)
else
status in
(*