From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:46:30 +0200 Subject: Use Maps and ids for universe binders Before sometimes there were lists and strings. --- engine/evd.mli | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 853a34bc4..36c399e98 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -502,12 +502,12 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : Universes.universe_binders -> UState.t - + val make_evar_universe_context : env -> (Id.t located) list option -> UState.t -val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map +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 -> string -> Univ.Level.t -val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_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 add_constraints_context : UState.t -> Univ.constraints -> UState.t @@ -519,9 +519,9 @@ val normalize_evar_universe_context_variables : UState.t -> val normalize_evar_universe_context : UState.t -> UState.t -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t -val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t -val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t +val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t +val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t val add_global_univ : evar_map -> Univ.Level.t -> evar_map -- cgit v1.2.3