From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 11 Feb 2004 16:02:18 +0000 (+0000)
Subject: bugfix: auto_disambiguation is not considered for searchPatternApply
X-Git-Tag: V_0_3_0~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eec68b7deed5396df14bd251127a96c46a868d06;p=helm.git

bugfix: auto_disambiguation is not considered for searchPatternApply
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c0aa8e830..08e6e539a 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -198,7 +198,7 @@ let
       (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
       uris)
  in
- if !auto_disambiguation then
+ if selection_mode <> `SINGLE && !auto_disambiguation then
   Lazy.force only_constant_choices
  else begin
    let choices = ref [] in