diff options
| author | Pierre-Marie Pédrot | 2015-10-29 13:04:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 13:11:38 +0100 |
| commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
| tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /engine/evd.mli | |
| parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
| parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index dc498ed42e..b295a431aa 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -259,10 +259,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map +val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Declareops.side_effects +val eval_side_effects : evar_map -> Safe_typing.private_constants (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map @@ -485,6 +485,9 @@ val evar_universe_context_subst : evar_universe_context -> Universes.universe_op val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val evar_universe_context_of_binders : + Universes.universe_binders -> evar_universe_context + val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map (** Raises Not_found if not a name for a universe in this map. *) @@ -532,7 +535,8 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context +val universe_context : ?names:(Id.t located) list -> evar_map -> + (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t |