From 43869b4e05824244e666c60e0b740a80e8b09d0c Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 28 Jun 2016 12:37:00 -0400 Subject: no-refold patch Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5. --- proofs/redexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8a9ce4f94..72cb05f1b 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -44,7 +44,7 @@ let cbv_native env sigma c = let whd_cbn flags env sigma t = let (state,_) = - (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty)) + (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) in Reductionops.Stack.zip ~refold:true state let strong_cbn flags = -- cgit v1.2.3