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/evd.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'engine/evd.mli') 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 -> -- cgit v1.2.3