) hyps,
(text,prefix_len,concl))
) seqs)
+ | GrafiteAst.NAuto (_loc, (l,a)) ->
+ NTactics.auto_tac
+ ~params:(List.map (fun x -> "",0,x) l,a)
| GrafiteAst.NCases (_loc, what, where) ->
NTactics.cases_tac
~what:(text,prefix_len,what)
let obj_kind =
NCicUntrusted.map_obj_kind
(NCicUntrusted.apply_subst subst []) obj_kind in
- let height = NCicUntrusted.height_of_obj_kind uri obj_kind in
+ let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
let obj = uri,height,[],[],obj_kind in
NCicTypeChecker.typecheck_obj obj;
NCicLibrary.add_obj uri obj;