]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: auto_disambiguation is not considered for searchPatternApply
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 11 Feb 2004 16:02:18 +0000 (16:02 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 11 Feb 2004 16:02:18 +0000 (16:02 +0000)
helm/gTopLevel/gTopLevel.ml

index c0aa8e830a20562d2ec55a4fae3264786793a70b..08e6e539aa7c1eb9922c0562cb66386a4c8fb2a2 100644 (file)
@@ -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