mathql query generator interface patched

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 6f6b854042f1be0d94d2f50c71b1112dca22a9bc..e3f49893171f5c9e1faaa01931ff9a76eef72a77 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1920,7 +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.searchPattern 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