Locate query changed again. There is a mismatch between Domenico's

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

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index b1c84ce10a483e414ad2e2ea44957397822f65ee..217f4d4d356b6eab0ab6f4b80dc457b61d258829 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -149,8 +149,13 @@ let close = Mqint.close
 
 let locate s = 
    let query = 
+(*CSC: next query to be fixed
+  1) I am exploiting the bug that does not quote '|'
+  2) I am searching only constants and mutual inductive definition blocks
+     (i.e. no fragment identifier at all)
+*)
       MQList (MQSelect ("ref", 
-                        MQPattern [(None, [MQBSS], [MQFSS])],
+                        MQPattern [(Some "cic", [MQBSS ; MQBC ".con|.ind"],[])],
                         MQIs (MQFunc (MQName, "ref"),
                               MQCons s
                              )