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/usage.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'sysinit/usage.ml')

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