diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-03 01:38:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-08 21:15:33 +0100 |
| commit | 67091e1d155be19333c5e5bd2cc306792ca630d3 (patch) | |
| tree | 04d89c833d37447ee2a02852fb887aedac1edc81 /pretyping/reductionops.mli | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
[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.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 3b56513f5..29dc3ed0f 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 |