From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 Sep 2005 16:55:02 +0000 (+0000)
Subject: Bug fixed: when several instances are tried during disambiguation, do not add
X-Git-Tag: V_0_1_2_1~9
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4384a12ff13352f8f87124f214072446164ed2b;p=helm.git

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 fe9cdca76..b7de40ed9 100644
--- 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 *)