diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 3 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
4 files changed, 23 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 69edb1498c..a5f81d1e59 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -479,6 +479,9 @@ let set_typing_flags c env = let env = set_type_in_type (not c.check_universes) env in env +let update_typing_flags ?typing_flags env = + Option.cata (fun flags -> set_typing_flags flags env) env typing_flags + let set_cumulative_sprop b env = set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env diff --git a/kernel/environ.mli b/kernel/environ.mli index 6a8ddce835..900e2128ea 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -351,6 +351,9 @@ val set_type_in_type : bool -> env -> env val set_allow_sprop : bool -> env -> env val sprop_allowed : env -> bool +(** [update_typing_flags ?typing_flags] may update env with optional typing flags *) +val update_typing_flags : ?typing_flags:typing_flags -> env -> env + val universes_of_global : env -> GlobRef.t -> AUContext.t (** {6 Sets of referred section variables } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6abd283f6c..a35f94e3ce 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -247,6 +247,15 @@ let set_native_compiler b senv = let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env } +(* Temporary sets custom typing flags *) +let with_typing_flags ?typing_flags senv ~f = + match typing_flags with + | None -> f senv + | Some typing_flags -> + let orig_typing_flags = Environ.typing_flags senv.env in + let res, senv = f (set_typing_flags typing_flags senv) in + res, set_typing_flags orig_typing_flags senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -928,6 +937,9 @@ let add_constant l decl senv = in kn, senv +let add_constant ?typing_flags l decl senv = + with_typing_flags ?typing_flags senv ~f:(add_constant l decl) + let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = @@ -983,6 +995,9 @@ let add_mind l mie senv = let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in kn, add_checked_mind kn mib senv +let add_mind ?typing_flags l mie senv = + with_typing_flags ?typing_flags senv ~f:(add_mind l mie) + (** Insertion of module types *) let add_modtype l params_mte inl senv = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 6fa9022906..287274e39a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -93,6 +93,7 @@ val export_private_constants : (** returns the main constant *) val add_constant : + ?typing_flags:Declarations.typing_flags -> Label.t -> global_declaration -> Constant.t safe_transformer (** Similar to add_constant but also returns a certificate *) @@ -102,6 +103,7 @@ val add_private_constant : (** Adding an inductive type *) val add_mind : + ?typing_flags:Declarations.typing_flags -> Label.t -> Entries.mutual_inductive_entry -> MutInd.t safe_transformer |