diff options
| author | Matthieu Sozeau | 2015-10-01 18:42:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:13 +0200 |
| commit | 4585baa53e7fa4c25e304b8136944748a7622e10 (patch) | |
| tree | b8a6b71eff51d1f1ef8367bdf420754597dcd8c3 /kernel/safe_typing.mli | |
| parent | de648c72a79ae5ba35db166575669ca465b11770 (diff) | |
Univs: refined handling of assumptions
According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2b4324b96f..b971a1bd42 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,7 +57,8 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 + (Id.t * Term.types * bool (* polymorphic *)) + Univ.in_universe_context_set -> safe_transformer0 val push_named_def : Id.t * Entries.definition_entry -> safe_transformer0 @@ -88,10 +89,10 @@ val add_modtype : (** Adding universe constraints *) val push_context_set : - Univ.universe_context_set -> safe_transformer0 + bool -> Univ.universe_context_set -> safe_transformer0 val push_context : - Univ.universe_context -> safe_transformer0 + bool -> Univ.universe_context -> safe_transformer0 val add_constraints : Univ.constraints -> safe_transformer0 |