let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
grafite_status,lexicon_status
in
let read_include_paths file =
grafite_status,lexicon_status
in
let read_include_paths file =