From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 25 Nov 2005 16:34:17 +0000 (+0000)
Subject: use empty universe in the mono alias phases
X-Git-Tag: make_still_working~8096
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b881e38c03d5ecf26267a47d7e4208bd31ebc33d;p=helm.git

use empty universe in the mono alias phases
---

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);