diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-21 11:55:32 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | 4838a3a3c25cc9f7583dd62e4585460aca8ee961 (patch) | |
| tree | 80a909def685c23e426d350d494bdc1f00165459 /kernel/environ.mli | |
| parent | 1cd87577ab85a402fb0482678dfcdbe85b45ce38 (diff) | |
Forcing i > Set for global universes (incomplete)
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 4ad0327fc..9f6ea522a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env (** Check constraints are satifiable in the environment. *) val check_constraints : Univ.constraints -> env -> bool -val push_context : Univ.universe_context -> env -> env -val push_context_set : Univ.universe_context_set -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env |