Don't lose names in UState.universe_context.

We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.

4 files changed, 71 insertions, 62 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 06b257a9e5..f1b5419dec 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -748,27 +748,10 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let universe_context ?names evd = UState.universe_context ?names evd.universes
-
-open Misctypes
-type universe_decl =
-  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-let check_implication evd cstrs ctx =
-  let uctx = evar_universe_context evd in
-  let gr = UState.initial_graph uctx in
-  let grext = UGraph.merge_constraints cstrs gr in
-  let cstrs' = Univ.UContext.constraints ctx in
-  if UGraph.check_constraints cstrs' grext then ()
-  else CErrors.user_err ~hdr:"check_univ_decl"
-                  (str "Universe constraints are not implied by the ones declared.")
-
-let check_univ_decl evd decl =
-  let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in
-  let pl, ctx = universe_context ?names:pl evd in
-  if not decl.univdecl_extensible_constraints then
-    check_implication evd decl.univdecl_constraints ctx;
-  pl, ctx
+let universe_context ~names ~extensible evd =
+  UState.universe_context ~names ~extensible evd.universes
+
+let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
 
 let restrict_universe_context evd vars =
   { evd with universes = UState.restrict evd.universes vars }
diff --git a/engine/evd.mli b/engine/evd.mli
index 8c3771cd94..abcabe8157 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -547,15 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : ?names:(Id.t located) list -> evar_map ->
+val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
 		       (Id.t * Univ.Level.t) list * Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
-type universe_decl =
-  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context
+val check_univ_decl : evar_map -> UState.universe_decl ->
+  Universes.universe_binders * Univ.universe_context
 
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 979a9b086b..13a9bb3732 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -257,41 +257,63 @@ let pr_uctx_level uctx =
       with Not_found | Option.IsNone ->
         Universes.pr_with_global_universes l
 
-let universe_context ?names ctx =
-  match names with
-  | None -> [], Univ.ContextSet.to_context ctx.uctx_local
-  | Some pl ->
-     let levels = Univ.ContextSet.levels ctx.uctx_local in
-     let newinst, map, left =
-       List.fold_right
-         (fun (loc,id) (newinst, map, acc) ->
-          let l =
-            try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
-            with Not_found ->
-              user_err ?loc ~hdr:"universe_context"
-                            (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
-          in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
-         pl ([], [], levels)
-     in
-       if not (Univ.LSet.is_empty left) then
-         let n = Univ.LSet.cardinal left in
-         let loc =
-           try
-             let info =
-               Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
-             info.uloc
-           with Not_found -> None
-         in
-           user_err ?loc ~hdr:"universe_context"
-                        ((str(CString.plural n "Universe") ++ spc () ++
-			     Univ.LSet.pr (pr_uctx_level ctx) left ++
-			   spc () ++ str (CString.conjugate_verb_to_be n) ++
-                           str" unbound."))
-      else
-        let inst = Univ.Instance.of_array (Array.of_list newinst) in
-        let ctx = Univ.UContext.make (inst,
-          Univ.ContextSet.constraints ctx.uctx_local)
-        in map, ctx
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let universe_context ~names ~extensible ctx =
+  let levels = Univ.ContextSet.levels ctx.uctx_local in
+  let newinst, left =
+    List.fold_right
+      (fun (loc,id) (newinst, acc) ->
+         let l =
+           try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+           with Not_found ->
+             user_err ?loc ~hdr:"universe_context"
+               (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+         in (l :: newinst, Univ.LSet.remove l acc))
+      names ([], levels)
+  in
+  if not extensible && not (Univ.LSet.is_empty left) then
+    let n = Univ.LSet.cardinal left in
+    let loc =
+      try
+        let info =
+          Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+        info.uloc
+      with Not_found -> None
+    in
+    user_err ?loc ~hdr:"universe_context"
+      ((str(CString.plural n "Universe") ++ spc () ++
+	Univ.LSet.pr (pr_uctx_level ctx) left ++
+	spc () ++ str (CString.conjugate_verb_to_be n) ++
+        str" unbound."))
+  else
+    let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
+    let inst = Array.append (Array.of_list newinst) left in
+    let inst = Univ.Instance.of_array inst in
+    let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in
+    let ctx = Univ.UContext.make (inst,
+                                  Univ.ContextSet.constraints ctx.uctx_local) in
+    map, ctx
+
+let check_implication uctx cstrs ctx =
+  let gr = initial_graph uctx in
+  let grext = UGraph.merge_constraints cstrs gr in
+  let cstrs' = Univ.UContext.constraints ctx in
+  if UGraph.check_constraints cstrs' grext then ()
+  else CErrors.user_err ~hdr:"check_univ_decl"
+      (str "Universe constraints are not implied by the ones declared.")
+
+let check_univ_decl uctx decl =
+  let open Misctypes in
+  let pl, ctx = universe_context
+      ~names:decl.univdecl_instance
+      ~extensible:decl.univdecl_extensible_instance
+      uctx
+  in
+  if not decl.univdecl_extensible_constraints then
+    check_implication uctx decl.univdecl_constraints ctx;
+  pl, ctx
 
 let restrict ctx vars =
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
diff --git a/engine/uState.mli b/engine/uState.mli
index 0b67bb71f8..21145e7e67 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -120,7 +120,13 @@ val normalize : t -> t
 
 (** {5 TODO: Document me} *)
 
-val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
+  (Id.t * Univ.Level.t) list * Univ.universe_context
+
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
 
 val update_sigma_env : t -> Environ.env -> t