From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 21 Sep 2017 11:14:11 +0200 Subject: Forbid repeated names in universe binders. --- engine/uState.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'engine/uState.ml') 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 = -- cgit v1.2.3