diff options
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 2b4324b96..b971a1bd4 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 |