Forbid repeated names in universe binders.

5 files changed, 4 insertions, 12 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 9ea2cc00f..0f17e0dc6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -935,9 +935,6 @@ let nf_constraints evd =
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s
 
-let add_universe_name evd s l =
-  { evd with universes = UState.add_universe_name evd.universes s l }
-
 let universe_binders evd = UState.universe_binders evd.universes
 
 let universes evd = UState.ugraph evd.universes
diff --git a/engine/evd.mli b/engine/evd.mli
index f06fb8d3b..c59a67039 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -509,7 +509,6 @@ val make_evar_universe_context : env -> (Id.t located) list option -> UState.t
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
-val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map
 
 val universe_binders : evar_map -> Universes.universe_binders
 val add_constraints_context : UState.t ->
diff --git a/engine/uState.ml b/engine/uState.ml
index dadc004c5..4e30640e4 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -109,6 +109,9 @@ let initial_graph ctx = ctx.uctx_initial_universes
 let algebraics ctx = ctx.uctx_univ_algebraic
 
 let add_uctx_names ?loc s l (names, names_rev) =
+  if UNameMap.mem s names
+  then user_err ?loc ~hdr:"add_uctx_names"
+      Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound.");
   (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
 
 let add_uctx_loc l loc (names, names_rev) =
@@ -573,10 +576,6 @@ let normalize uctx =
 let universe_of_name uctx s = 
   UNameMap.find s (fst uctx.uctx_names)
 
-let add_universe_name uctx s l =
-  let names' = add_uctx_names s l uctx.uctx_names in
-  { uctx with uctx_names = names' }
-
 let update_sigma_env uctx env =
   let univs = Environ.universes env in
   let eunivs =
diff --git a/engine/uState.mli b/engine/uState.mli
index 4265f2b20..16fba41e0 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -80,9 +80,6 @@ val add_universe_constraints : t -> Universes.universe_constraints -> t
 
 (** {5 Names} *)
 
-val add_universe_name : t -> Id.t -> Univ.Level.t -> t
-(** Associate a human-readable name to a local variable. *)
-
 val universe_of_name : t -> Id.t -> Univ.Level.t
 (** Retrieve the universe associated to the name. *)
 
diff --git a/engine/universes.ml b/engine/universes.ml
index f2942be6d..5ac1bc685 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -55,7 +55,7 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj
 let register_universe_binders ref ubinders =
   (* Add the polymorphic (section) universes *)
   let open Names in
-  let ubinders = Idmap.fold (fun id (poly,lvl) ubinders ->
+  let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders ->
       if poly then Id.Map.add id lvl ubinders
       else ubinders)
       (fst (Global.global_universe_names ())) ubinders