Fix #7539: Checker does not properly handle negative coinductive types.

The reduction machine of the checker was not taking into account the fact
that cofixpoints needed to be unfolded when applied against a projection.

1 files changed, 26 insertions, 0 deletions

diff --git a/test-suite/coqchk/bug_7539.v b/test-suite/coqchk/bug_7539.v
new file mode 100644
index 000000000..74ebe9290
--- /dev/null
+++ b/test-suite/coqchk/bug_7539.v
@@ -0,0 +1,26 @@
+Set Primitive Projections.
+
+CoInductive Stream : Type := Cons { tl : Stream }.
+
+Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
+  match n with
+  | O => s
+  | S m => Str_nth_tl m (tl s)
+  end.
+
+CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
+  eqst_tl : EqSt (tl s1) (tl s2);
+}.
+
+Axiom EqSt_reflex : forall (s : Stream), EqSt s s.
+
+CoFixpoint map (s:Stream) : Stream := Cons (map (tl s)).
+
+Lemma Str_nth_tl_map : forall n s, EqSt (Str_nth_tl n (map s)) (map (Str_nth_tl n s)).
+Proof.
+induction n.
++ intros; apply EqSt_reflex.
++ cbn; intros s; apply IHn.
+Qed.
+
+Definition boom : forall s, tl (map s) = map (tl s) := fun s => eq_refl.