diff options
| author | Maxime Dénès | 2017-09-26 23:57:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-26 23:57:40 +0200 |
| commit | b9740771e8113cb9e607793887be7a12587d0326 (patch) | |
| tree | f69105ad9813738abd10ae824756947940a7dc6d /engine/evd.mli | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
| parent | 3c964a60d698134c21adc77cbb69ce1528350682 (diff) | |
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 3f00a3b0b2..abcabe8157 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : @@ -547,11 +547,13 @@ 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 -> +val universe_context : names:(Id.t located) list -> extensible:bool -> 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 +val check_univ_decl : evar_map -> UState.universe_decl -> + Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map |