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)
---
 vernac/vernacentries.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index cf233248d7..2ac8458ad5 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -26,4 +26,3 @@ 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
-- 
cgit v1.2.3