diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-04-13 20:41:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-04-13 20:47:06 +0200 |
| commit | 58e804f07172acc6bb01c8bdafde1217eb4ec4b8 (patch) | |
| tree | cf6057cb340cf71867f04b19b0f7733596949b1c /pretyping/reductionops.ml | |
| parent | 582fab072375924ce380148c8a92dbc2b4ec30cc (diff) | |
Reinstate fixpoint refolding in [cbn], deactivated by mistake.
Add a test-suite file to be sure we won't regress silently.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 297f0a1a8..ba92f64b9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -755,7 +755,7 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty context" in contract_fix *) let reduce_and_refold_fix recfun env refold cst_l fix sk = let raw_answer = - let env = if refold then None else Some env in + let env = if refold then Some env else None in contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in apply_subst (fun x (t,sk') -> |