From df7d00971e430468cbf57fa6119b7ed5149a9193 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 4 Feb 2021 12:22:59 +0100
Subject: Remove deprecated -sprop-cumulative command line argument

Deprecated since #12034 (8.12)
---
 sysinit/coqargs.ml | 7 -------
 sysinit/usage.ml   | 1 -
 2 files changed, 8 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index c4f12f6bb7..57658a1eac 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -184,10 +184,6 @@ let set_query opts q =
   | Queries queries -> Queries (queries@[q])
   }
 
-let warn_deprecated_sprop_cumul =
-  CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
-         (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
-
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
@@ -419,9 +415,6 @@ let parse_args ~usage ~init arglist : t * string list =
       add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
     |"-disallow-sprop" ->
       add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
-    |"-sprop-cumulative" ->
-      warn_deprecated_sprop_cumul();
-      add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
diff --git a/sysinit/usage.ml b/sysinit/usage.ml
index 1831a3f9b2..763cd54137 100644
--- a/sysinit/usage.ml
+++ b/sysinit/usage.ml
@@ -79,7 +79,6 @@ let print_usage_common co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -allow-sprop           allow using the proof irrelevant SProp sort\
 \n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
-\n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
-- 
cgit v1.2.3