- | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a)
+ | GrafiteAst.NAuto (_loc, (None,a)) ->
+ NAuto.auto_tac ~params:(None,a) ?trace_ref:None
- ~params:(Some List.map (fun x -> "",0,x) l,a)
+ ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
| GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
| GrafiteAst.NCases (_loc, what, where) ->
NTactics.cases_tac
| GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
| GrafiteAst.NCases (_loc, what, where) ->
NTactics.cases_tac
| 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.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.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
| 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
NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
| GrafiteAst.NInversion (_loc, what, where) ->
NTactics.inversion_tac
~what:(text,prefix_len,what)
| GrafiteAst.NInversion (_loc, what, where) ->
NTactics.inversion_tac
~what:(text,prefix_len,what)
| _ -> obj_kind
in
let obj = uri,height,[],[],obj_kind in
| _ -> obj_kind
in
let obj = uri,height,[],[],obj_kind in