Merge PR #10199: Fix computation of implicit arguments when names collide in local fix/cofix (#10197)

Reviewed-by: maximedenes

2 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10197.v b/test-suite/bugs/closed/bug_10197.v
new file mode 100644
index 0000000000..920c5f5cb7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10197.v
@@ -0,0 +1,16 @@
+(* Some check about implicit arguments in fix *)
+
+Check fix f {f:nat} := match f with 0 => true | _ => false end.
+
+CoInductive stream := { this : nat ; next : option stream }.
+
+Check cofix f {f:nat} := {| this := f ; next := None |}.
+
+(* The following was ok from 8.4, just checking that the order is not
+   mixed up accidentally *)
+
+Check fix f (x : nat) (x : forall {a:nat}, a = 0 -> nat) :=
+   match x eq_refl with 0 => true | _ => false end.
+
+Check fix f (x : forall {a:nat}, a = 0 -> bool) (x : nat) :=
+   match x with 0 => true | _ => false end.
diff --git a/test-suite/bugs/closed/bug_3810.v b/test-suite/bugs/closed/bug_3810.v
new file mode 100644
index 0000000000..0b2bef8a9b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3810.v
@@ -0,0 +1,6 @@
+Class Foo.
+
+Fixpoint test (H : Foo) (n : nat) {A : Type} {struct n} : A.
+Admitted.
+
+Check fun (x:Foo) => test x 0.