From c31fdc4a69f64c79fc98633fa8768e21d3cffada Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Jun 2002 08:51:42 +0000 Subject: [PATCH] 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. --- helm/gTopLevel/mQueryGenerator.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 ) -- 2.39.2