From e4384a12ff13352f8f87124f214072446164ed2b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 Sep 2005 16:55:02 +0000 Subject: [PATCH] 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). --- helm/matita/matitaDisambiguator.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 *) -- 2.39.2