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

2 files changed, 27 insertions, 1 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index 66e69f225..b9ae4daa8 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -754,7 +754,7 @@ let rec knr info m stk =
        | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((ZcaseT _)::_) as stk')) ->
+          (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
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.