From 36a85ffd9542d5a726d154cd8bf37d417da2cf88 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 31 Oct 2002 14:24:15 +0000 Subject: [PATCH] MQueryGenerator ported to use fun "objectName" topLevel typechecker output was removed --- helm/gTopLevel/mQueryGenerator.ml | 2 +- helm/gTopLevel/topLevel/topLevel.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index 4deaf8c7a..9f52c2f20 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -185,7 +185,7 @@ let execute_query query = let locate s = let module M = MathQL in - let q = M.Ref (M.Fun "reference" (M.Const [s])) in + let q = M.Ref (M.Fun "objectName" (M.Const [s])) in execute_query q let backward e c t level = diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml index d53ea70ea..6db896d9b 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -196,7 +196,7 @@ let _ = CicCooking.init () ; Logger.log_callback := (Logger.log_to_html - ~print_and_flush:(function s -> print_string s ; flush stdout)) ; + ~print_and_flush:(function s -> () (* print_string s ; flush stdout *) )); Mqint.set_stat false; Gen.set_log_file "MQGenLog.htm"; set_dbms 1; -- 2.39.2