Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fixpoint` with a let binder

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_3282.v b/test-suite/bugs/closed/bug_3282.v
index ce7cab1cba..f32e0969c8 100644
--- a/test-suite/bugs/closed/bug_3282.v
+++ b/test-suite/bugs/closed/bug_3282.v
@@ -5,3 +5,25 @@ Definition foo := fix f (m : nat) (o := true) (n : nat) {struct n} :=
 
 Fixpoint f (m : nat) (o := true) (n : nat) {struct n} :=
   match n with 0 => 0 | S n' => f 0 n' end.
+
+Definition foo' := fix f {m : nat} (o := true) (n : nat) {struct n} :=
+  match n with 0 => 0 | S n' => f (m:=0) n' end.
+Check foo' (m:=0) 0.
+
+Fixpoint f' {m : nat} (o := true) (n : nat) {struct n} :=
+  match n with 0 => 0 | S n' => f' (m:=0) n' end.
+Check f' (m:=0) 0.
+
+CoInductive Stream := { hd : nat; tl : Stream }.
+
+Definition cofoo := cofix f (o := true) {m} := {| hd := 0; tl := f (m:=0) |}.
+Check cofoo (m:=0).
+
+CoFixpoint cof (o := true) {m} := {| hd := 0; tl := cof (m:=0) |}.
+Check cof (m:=0).
+
+Definition cofoo' := cofix f {m} (o := true) := {| hd := 0; tl := f (m:=0) |}.
+Check cofoo' (m:=0).
+
+CoFixpoint cof' {m} (o := true) := {| hd := 0; tl := cof' (m:=0) |}.
+Check cof' (m:=0).