From b881e38c03d5ecf26267a47d7e4208bd31ebc33d Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 25 Nov 2005 16:34:17 +0000
Subject: [PATCH] use empty universe in the mono alias phases

---
 helm/matita/matitaDisambiguator.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 24a835523..0f4dc67db 100644
--- 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);
-- 
2.39.2