X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;fp=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=181532462b7b370140297ee48a119e7510e30991;hb=7c24781a5668273116bb64e93e56f4ab1ab3fede;hp=76d44421c62452edb280d6e0bad8b7e9f7c2f496;hpb=e1dee095df33ef99ad011bc30eeb256f31ffdf10;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 76d44421c..181532462 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -108,8 +108,8 @@ let disambiguate_thing ~aliases ~universe
     f ~fresh_instances ~aliases ~universe thing
   in
   let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
-   if use_mono_aliases && not instances then
-    drop_aliases res
+   if use_mono_aliases then
+    drop_aliases ~minimize_instances:true res (* one shot aliases *)
    else if user_asked then
     drop_aliases ~minimize_instances:true res (* one shot aliases *)
    else