1 files changed, 15 insertions, 10 deletions
diff --git a/checker/univ.ml b/checker/univ.ml
index 1619010c..a0511ad2 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -142,7 +142,13 @@ end
 
 (** Level sets and maps *)
 module LMap = HMap.Make (Level)
-module LSet = LMap.Set
+module LSet = struct
+  include LMap.Set
+
+  let pr s =
+    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+
+end
 
 type 'a universe_map = 'a LMap.t
 
@@ -301,7 +307,7 @@ struct
 
   let for_all = List.for_all
 
-  let smartmap = List.smartmap
+  let smart_map = List.Smart.map
 
 end
 
@@ -863,12 +869,12 @@ struct
   let is_empty x = Int.equal (Array.length x) 0
 
   let subst_fn fn t = 
-    let t' = CArray.smartmap fn t in
+    let t' = CArray.Smart.map fn t in
       if t' == t then t else t'
 
   let subst s t =
     let t' = 
-      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+      CArray.Smart.map (fun x -> try LMap.find x s with Not_found -> x) t
     in if t' == t then t else t'
 
   let pr =
@@ -904,11 +910,11 @@ let subst_instance_level s l =
   | _ -> l
 
 let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
+  Array.Smart.map (fun l -> subst_instance_level s l) i
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1049,7 +1055,7 @@ let subst_univs_level_level subst l =
 
 let subst_univs_level_universe subst u =
   let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1082,14 +1088,13 @@ let subst_univs_universe fn ul =
 
 let merge_context strict ctx g =
   let g = Array.fold_left
-   (* Be lenient, module typing reintroduces universes and 
-      constraints due to includes *)
-	    (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+            (fun g v -> add_universe v strict g)
 	    g (UContext.instance ctx)
   in merge_constraints (UContext.constraints ctx) g
 
 let merge_context_set strict ctx g =
   let g = LSet.fold
+   (* Include and side effects still have double-declared universes *)
 	    (fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
 	    (ContextSet.levels ctx) g
   in merge_constraints (ContextSet.constraints ctx) g