use empty universe in the mono alias phases

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 24a8355237b7d1e4a7b81d4b58068a01537bc22d..0f4dc67db6b9fafc977d414b3f7e85f5a79b729e 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -80,8 +80,8 @@ let disambiguate_thing ~aliases ~universe
 =
   assert (universe <> None);
   let library = false, DisambiguateTypes.Environment.empty, None in
-  let multi_aliases=false, DisambiguateTypes.Environment.empty, universe in
-  let mono_aliases = true, aliases, None in
+  let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+  let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
   let passes =  (* <fresh_instances?, aliases, coercions?> *)
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);