X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=a941bf0883476f87144b7fdafcb3dab8ff59725d;hb=de9926defa9fdb4aaebbad4f4131b7704602597b;hp=7768e2287f27d5626262c3b6a7f583d2a272e3dc;hpb=441cd9b8db014ea11f5afc46f192a3d73eee6a39;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 7768e2287..a941bf088 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -512,7 +512,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
         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 = 
@@ -675,7 +676,7 @@ let initial_statuses baseuri =
    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 =