| 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)
| GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
| GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
| GrafiteAst.NTry (_,tac) -> NTactics.try_tac
- (aux f (text, prefix_len, tac))
+ (f f (text, prefix_len, tac))
| GrafiteAst.NAssumption _ -> NTactics.assumption_tac
| GrafiteAst.NBlock (_,l) ->
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
| _ -> 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
(*