diff options
| author | Pierre-Marie Pédrot | 2020-04-23 14:53:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 14:53:23 +0200 |
| commit | 48f73e492465f3c46438583c069bc0ba745ef56f (patch) | |
| tree | e499cc660630fcadd08aff5a127a8c34455d664d /library | |
| parent | 7863c12930687e1e2dc982d9b406fb4d6e7a02c1 (diff) | |
| parent | 3231196c77c0641d7c59191bf691378b334afc46 (diff) | |
Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index abc04a5e14..5c847fda96 100644 --- a/library/global.ml +++ b/library/global.ml @@ -99,7 +99,9 @@ let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) let set_check_universes c = globalize0 (Safe_typing.set_check_universes c) let typing_flags () = Environ.typing_flags (env ()) -let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative +let set_cumulative_sprop b = + set_typing_flags {(typing_flags()) with Declarations.cumulative_sprop = b} +let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) diff --git a/library/global.mli b/library/global.mli index e7133a1034..2acd7e2a67 100644 --- a/library/global.mli +++ b/library/global.mli @@ -36,7 +36,8 @@ val set_check_guarded : bool -> unit val set_check_positive : bool -> unit val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags -val make_sprop_cumulative : unit -> unit +val set_cumulative_sprop : bool -> unit +val is_cumulative_sprop : unit -> bool val set_allow_sprop : bool -> unit val sprop_allowed : unit -> bool |