Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/6129.v b/test-suite/bugs/closed/6129.v
new file mode 100644
index 00000000..e4a2a2ba
--- /dev/null
+++ b/test-suite/bugs/closed/6129.v
@@ -0,0 +1,9 @@
+(* Make definition of coercions compatible with local definitions. *)
+
+Record foo (x : Type) (y:=1) := { foo_nat :> nat }.
+Record foo2 (x : Type) (y:=1) (z t: Type) := { foo_nat2 :> nat }.
+Record foo3 (y:=1) (z t: Type) := { foo_nat3 :> nat }.
+
+Check fun x : foo nat => x + 1.
+Check fun x : foo2 nat nat nat => x + 1.
+Check fun x : foo3 nat nat => x + 1.