diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 7ce1cea27..0edcb34de 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -50,6 +50,7 @@ val set_opaque_tables : env -> Opaqueproof.opaquetab -> env val engagement : env -> engagement +val typing_flags : env -> typing_flags val is_impredicative_set : env -> bool val type_in_type : env -> bool @@ -214,6 +215,7 @@ 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 +val set_typing_flags : typing_flags -> env -> env (** {6 Sets of referred section variables } [global_vars_set env c] returns the list of [id]'s occurring either |