diff options
| author | Matthieu Sozeau | 2019-12-13 11:40:48 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-12-13 11:40:48 +0100 |
| commit | 3c24d4f6398cc80fd070c4e6dcac99670c8c1bba (patch) | |
| tree | 5196448bc356711cd3924dc7f80e2908558d9238 /kernel/environ.mli | |
| parent | dd47dfc29f4b38dd2b1745ecbf452c3cd459b89b (diff) | |
Use ~strict argument consistently in push_context/push_context_set intfs
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 257bd43083..bd5a000c2b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -296,7 +296,13 @@ val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) val check_constraints : Univ.Constraint.t -> env -> bool val push_context : ?strict:bool -> Univ.UContext.t -> env -> env +(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment. + @raise UGraph.AlreadyDeclared if one of the universes is already declared. +*) val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env +(* [push_context_set ?(strict=false) ctx env] pushes the universe context set + to the environment. It does not fail if one of the universes is already declared. *) + val push_constraints_to_env : 'a Univ.constrained -> env -> env val push_subgraph : Univ.ContextSet.t -> env -> env |