X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=e3f49893171f5c9e1faaa01931ff9a76eef72a77;hb=a48c5f0f412bbb8c1d6601dd5e11e5c3746f11d5;hp=83947a24abad3abde38ee1097d63f14c2020dc5c;hpb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 83947a24a..e3f498931 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -43,10 +43,7 @@ module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
-(*
 let mqi_flags = [] (* default MathQL interpreter options *)
-*)
 let mqi_handle = MQIC.init mqi_flags prerr_string
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
@@ -1923,16 +1920,7 @@ let completeSearchPattern () =
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = MQueryLevels2.get_constraints expr in
    let must',only = refine_constraints must in
-   let query =
-    MQG.query_of_constraints
-     (Some
-       ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
-        "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
-        "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
-        "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
-       ])
-     must' only
-   in
+   let query = MQG.query_of_constraints None must' only in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
   with