From 14dbb9ba574d4923b31ae31db3e749b31091d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 4 Dec 2007 15:16:25 +0000 Subject: [PATCH] do_heavy_checks not always true, take ths option from the registry instead --- helm/software/matita/matitaScript.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2