Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (EDIT: for mutual fixpoints)

2 files changed, 19 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') ->
diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
new file mode 100644
index 000000000..6aeb05f54
--- /dev/null
+++ b/test-suite/success/cbn.v
@@ -0,0 +1,18 @@
+(* cbn is able to refold mutual recursive calls *)
+
+Fixpoint foo (n : nat) :=
+  match n with
+  | 0 => true
+  | S n => g n
+  end
+with g (n : nat) : bool :=
+  match n with
+  | 0 => true
+  | S n => foo n
+  end.
+Goal forall n, foo (S n) = g n.
+  intros. cbn.
+  match goal with
+    |- g _ = g _ => reflexivity
+  end.
+Qed.
\ No newline at end of file