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

---
 kernel/declareops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 20dc21900c..b347152c16 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
+  cumulative_sprop = false;
 }
 
 (** {6 Arities } *)
-- 
cgit v1.2.3