Bug fixed: when several instances are tried during disambiguation, do not add

aliases unless they are absolutely necessary. Even in this case they should
be one-shot aliases (not implemented yet).

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index fe9cdca761785a081c3ae18e84addbe68bd27ae9..b7de40ed966eb580740c5b506f4bb53103180b4e 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -90,8 +90,8 @@ let disambiguate_thing ~aliases
     CoercDb.use_coercions := use_coercions;
     f ~fresh_instances ~aliases thing
   in
-  let set_aliases (_,(use_multi_aliases,_),_) (_, user_asked as res) =
-   if not use_multi_aliases then
+  let set_aliases (instances,(use_multi_aliases,_),_) (_, user_asked as res) =
+   if not use_multi_aliases && not instances then
     res
    else if user_asked then
     res (* one shot aliases *)