diff options
| author | Emilio Jesus Gallego Arias | 2020-10-16 20:06:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-26 21:21:55 +0100 |
| commit | 2ac3d11f6f1332250e918ef628eca3b788b3550a (patch) | |
| tree | dc14ffc3f4f2331a0960b4fad0d872d765257c10 /kernel/environ.ml | |
| parent | 454a10da9412a5bd6f3661b1f60e17f08289d0e5 (diff) | |
[environ] [typing_flags] Introduce helper function to remove duplicate code
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 3 |
1 files changed, 3 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 |