let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
- ~universe:grafite_status.GrafiteTypes.universe) proof_status
+ ~automation_cache:grafite_status.GrafiteTypes.automation_cache)
+ proof_status
in
let proof_term =
let irl =
CicNotation2.load_notation ~include_paths:[]
BuildTimeConf.core_notation_script
in
- let grafite_status = GrafiteSync.init baseuri in
+ let grafite_status = GrafiteSync.init lexicon_status baseuri in
grafite_status,lexicon_status
in
let read_include_paths file =