Merge PR #1033: Universe binder improvements

3 files changed, 14 insertions, 17 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 1a589897bd..1b4645aff6 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -203,12 +203,9 @@ let declare_constant_common id cst =
   update_tables c;
   c
 
+let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
-  let univs =
-    if poly then Polymorphic_const_entry univs
-    else Monomorphic_const_entry univs
-  in
+    ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
@@ -261,9 +258,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
 
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
-  ?(poly=false) id ?types (body,ctx) =
+  id ?types (body,univs) =
   let cb =
-    definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
+    definition_entry ?types ~univs ~opaque body
   in
     declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
@@ -340,7 +337,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_record = None;
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
-  mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
+  mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
   mind_entry_private = None;
 })
 
@@ -457,16 +454,16 @@ let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
 (* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.Level.t) list
+type universe_decl = polymorphic * Universes.universe_binders
 
 let cache_universes (p, l) =
   let glob = Global.global_universe_names () in
   let glob', ctx =
-    List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
+    Id.Map.fold (fun id lev ((idl,lid),ctx) ->
         ((Id.Map.add id (p, lev) idl,
           Univ.LMap.add lev id lid),
          Univ.ContextSet.add_universe lev ctx))
-      (glob, Univ.ContextSet.empty) l
+      l (glob, Univ.ContextSet.empty)
   in
   cache_universe_context (p, ctx);
   Global.set_global_universe_names glob'
@@ -487,9 +484,9 @@ let do_universe poly l =
                    (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
-    List.map (fun (l, id) ->
+    List.fold_left (fun acc (l, id) ->
 	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-	      (id, lev)) l
+              Id.Map.add id lev acc) Id.Map.empty l
   in
     Lib.add_anonymous_leaf (input_universes (poly, l))
 
diff --git a/interp/declare.mli b/interp/declare.mli
index 9b3194dec5..d50d37368c 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -42,7 +42,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?poly:polymorphic -> ?univs:Univ.UContext.t ->
+  ?univs:Entries.constant_universes_entry ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -56,8 +56,8 @@ val declare_constant :
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
-  constr Univ.in_universe_context_set -> Constant.t
+  ?local:bool -> Id.t -> ?types:constr ->
+  constr Entries.in_constant_universes_entry -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 08657936ee..3eb91d8cd7 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,7 +62,7 @@ let transl_with_decl env = function
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
     let c, ectx = interp_constr env (Evd.from_env env) c in
-    let ctx = Evd.evar_context_universe_context ectx in
+    let ctx = UState.context ectx in
       WithDef (fqid,(c,ctx))
 
 let loc_of_module l = l.CAst.loc