From fbbcea2eda411fbacfafdeec3266a19af17935f3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 4 Jul 2017 17:11:45 +0200
Subject: Deprecate options that were introduced for compatibility with 8.5.

---
 pretyping/reductionops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cc1709f1c2..ce9ca93d90 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,7 +29,7 @@ exception Elimconst
 
 let refolding_in_reduction = ref false
 let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
+  Goptions.optdepr = true; (* remove in 8.8 *)
   Goptions.optname =
     "Perform refolding of fixpoints/constants like cbn during reductions";
   Goptions.optkey = ["Refolding";"Reduction"];
-- 
cgit v1.2.3