From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 15:16:25 +0000 (+0000)
Subject: do_heavy_checks not always true, take ths option from the registry instead
X-Git-Tag: make_still_working~5734
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=14dbb9ba574d4923b31ae31db3e749b31091d24a;p=helm.git

do_heavy_checks not always true, take ths option from the registry instead
---

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index c29e15533..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