Added an option --enable-annot to the configure to compile with -dtypes

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 3ff2d034901f15bbf175e2630dc993d90d3356f8..9fb92c274f60367287ec20849e6c2ace90001c62 100644 (file)
--- 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 = 
@@ -568,7 +569,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
           raise exn
           (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
   | TA.Inline (_,style,suri,prefix,flavour) ->
-       let str = 
+       let str = "\n\n" ^ 
          ApplyTransformation.txt_of_inline_macro
           ~map_unicode_to_tex:(Helm_registry.get_bool
             "matita.paste_unicode_as_tex")