]> matita.cs.unibo.it Git - helm.git/commitdiff
Aliases are now wrote down even during the first pass.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Sep 2006 13:40:01 +0000 (13:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Sep 2006 13:40:01 +0000 (13:40 +0000)
The only case they are not written down is that of multiple passes.
This makes the scripts more robusts and faster.
We still need (more and more) one shot aliases.

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