From e8ccf6120f3765e04c527bca8b2b1fffc6df08ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Aug 2018 14:59:23 +0200
Subject: Fixing #8270 (cbn was calling zeta even when not asked for).

---
 pretyping/reductionops.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 07eeec9276..dd3cd26f0f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -144,6 +144,9 @@ val pr_state : state -> Pp.t
 
 (** {6 Reduction Function Operators } *)
 
+val strong_with_flags :
+  (CClosure.RedFlags.reds -> reduction_function) ->
+  (CClosure.RedFlags.reds -> reduction_function)
 val strong : reduction_function -> reduction_function
 val local_strong : local_reduction_function -> local_reduction_function
 val strong_prodspine : local_reduction_function -> local_reduction_function
-- 
cgit v1.2.3