From 67091e1d155be19333c5e5bd2cc306792ca630d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 3 Mar 2018 01:38:19 +0100
Subject: [compat] Remove "Refolding Reduction" option.

Following up on #6791, we remove support refolding in reduction.

We also update a test case that was not properly understood, see the
discussion in #6895.
---
 pretyping/reductionops.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 3b56513f5e..29dc3ed0f2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -31,11 +31,6 @@ module ReductionBehaviour : sig
   val print : Globnames.global_reference -> Pp.t
 end
 
-(** Option telling if reduction should use the refolding machinery of cbn
-   (off by default) *)
-val get_refolding_in_reduction : unit -> bool
-val set_refolding_in_reduction : bool -> unit
-
 (** {6 Support for reduction effects } *)
 
 type effect_name = string
-- 
cgit v1.2.3