New policy for the disambiguation passes.

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index db69cb71dfdd0eedf5050d3f03278e4106c24084..fe9cdca761785a081c3ae18e84addbe68bd27ae9 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -73,13 +73,14 @@ let disambiguate_thing ~aliases
   ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
   (thing: 'a)
 =
-  let library = false, DisambiguateTypes.empty_environment in
+  let library = true, DisambiguateTypes.empty_environment in
   let multi_aliases = true, aliases in
   let mono_aliases = false, aliases in
   let passes =  (* <fresh_instances?, aliases, coercions?> *)
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);
-      (true, library, false);
+      (true, mono_aliases, false);
+      (true, multi_aliases, false);
       (true, mono_aliases, true);
       (true, multi_aliases, true);
       (true, library, true);
@@ -89,15 +90,21 @@ 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
+    res
+   else if user_asked then
+    res (* one shot aliases *)
+   else
+    set_aliases aliases res
+  in
   let rec aux =
     function
-    | [ pass ] -> try_pass pass
+    | [ pass ] -> set_aliases pass (try_pass pass)
     | hd :: tl ->
         (try
-          try_pass hd
-        with Disambiguate.NoWellTypedInterpretation ->
-          let (_, user_asked) as res = aux tl in
-          if user_asked then res else set_aliases aliases res)
+          set_aliases hd (try_pass hd)
+        with Disambiguate.NoWellTypedInterpretation -> aux tl)
     | [] -> assert false
   in
   let saved_use_coercions = !CoercDb.use_coercions in