diff options
| -rw-r--r-- | engine/evd.ml | 3 | ||||
| -rw-r--r-- | engine/evd.mli | 1 | ||||
| -rw-r--r-- | engine/uState.ml | 7 | ||||
| -rw-r--r-- | engine/uState.mli | 3 | ||||
| -rw-r--r-- | engine/universes.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 2 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.v | 3 |
7 files changed, 9 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 diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 04bd169bd..a2857294b 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -53,6 +53,8 @@ Monomorphic mono = Type@{u} (* {u} |= *) mono is not universe polymorphic +The command has indeed failed with message: +Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1, M+1, N+1)} diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index f0a990986..013f215b5 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -34,6 +34,9 @@ Print foo. Monomorphic Definition mono@{u} := Type@{u}. Print mono. +(* fun x x => foo is nonsense with local binders *) +Fail Definition fo@{u u} := Type@{u}. + (* Using local binders for printing. *) Print foo@{E M N}. (* Underscores discard the name if there's one. *) |