diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ea45f699ce..6970a11e72 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,18 @@ let set_typing_flags c senv = if env == senv.env then senv else { senv with env } +let set_check_guarded b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_guarded = b } senv + +let set_check_positive b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_positive = b } senv + +let set_check_universes b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_universes = b } senv + let set_indices_matter indices_matter senv = set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv |