added the support for the "Locate Inductive Principles" query

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ec19107dde4e030dc56bb6311e324a7ad61b0227..65f381859e299bea48c0c669ec5bd76665214bf6 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1916,7 +1916,7 @@ let completeSearchPattern () =
    let must = CGSearchPattern.get_constraints expr in
    let must',only = refine_constraints must in
    let query =
-    MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+    MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
    in
    let results = MQI.execute mqi_handle query in 
     show_query_results results