From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jun 2016 18:25:02 +0200 Subject: Moving the typing_flags to the environment. --- kernel/environ.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/environ.mli') 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 -- cgit v1.2.3