diff options
| author | Gaëtan Gilbert | 2020-04-06 14:41:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 23:10:03 +0200 |
| commit | 3231196c77c0641d7c59191bf691378b334afc46 (patch) | |
| tree | aa10bcb9d93072e4808e831d4e4a73f88ad47349 /vernac | |
| parent | 988e195c2cd0d97b664193bf1c83c3da2b380f7c (diff) | |
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 14 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 1 |
2 files changed, 12 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 044e479aeb..c4c1c2935c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1302,6 +1302,7 @@ let vernac_generalizable ~local = Implicit_quantifiers.declare_generalizable ~local let allow_sprop_opt_name = ["Allow";"StrictProp"] +let cumul_sprop_opt_name = ["Cumulative";"StrictProp"] let () = declare_bool_option @@ -1313,6 +1314,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = cumul_sprop_opt_name; + optread = Global.is_cumulative_sprop; + optwrite = Global.set_cumulative_sprop } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } @@ -1487,21 +1495,21 @@ let () = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } -let _ = +let () = declare_bool_option { optdepr = false; optkey = ["Guard"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); optwrite = (fun b -> Global.set_check_guarded b) } -let _ = +let () = declare_bool_option { optdepr = false; optkey = ["Positivity"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); optwrite = (fun b -> Global.set_check_positive b) } -let _ = +let () = declare_bool_option { optdepr = false; optkey = ["Universe"; "Checking"]; diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 2ac8458ad5..cf233248d7 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -26,3 +26,4 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr val command_focus : unit Proof.focus_kind val allow_sprop_opt_name : string list +val cumul_sprop_opt_name : string list |