]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteDisambiguator.ml
Aliases are now wrote down even during the first pass.
[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguator.ml
index 76d44421c62452edb280d6e0bad8b7e9f7c2f496..181532462b7b370140297ee48a119e7510e30991 100644 (file)
@@ -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