X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=8ec2a4948bcc7c6bc19608d03f59a1089aa0468f;hb=b89690596acb0b24f1fd45da28ac04b4ad217e98;hp=a007e70237913407bf3fc42e4fdb9444679fcf4a;hpb=0ad4c9bd12acf983a6490bf783f69fcbbab42989;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a007e7023..8ec2a4948 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -85,7 +85,8 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let text = skipped_txt ^ nonskipped_txt in
   let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
   let enriched_history_fragment =
-   MatitaEngine.eval_ast ~do_heavy_checks:true
+   MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
+     "matita.do_heavy_checks")
     lexicon_status grafite_status (text,prefix_len,st)
   in
   let enriched_history_fragment = List.rev enriched_history_fragment in
@@ -488,6 +489,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       let proof_status = proof,user_goal' in
       if rewrite then
         let l = MQ.equations_for_goal ~dbd proof_status in
+        let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in
         let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in
         guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
         [], "", parsed_text_length