From 3231196c77c0641d7c59191bf691378b334afc46 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Apr 2020 14:41:45 +0200
Subject: Make cumulative sprop a typing flag, deprecate command line
 -sprop-cumulative

---
 library/global.ml  | 4 +++-
 library/global.mli | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'library')

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
 
-- 
cgit v1.2.3