From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 25 Jun 2002 08:51:42 +0000 (+0000)
Subject: Locate query changed again. There is a mismatch between Domenico's
X-Git-Tag: V_0_3_0_debian_8~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c31fdc4a69f64c79fc98633fa8768e21d3cffada;p=helm.git

Locate query changed again. There is a mismatch between Domenico's
implementation and Ferruccio's semantics. The code now conforms to
Domenico's implementation and seems to work.
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index b1c84ce10..217f4d4d3 100644
--- 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
                              )