Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of record fields.

3 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index c012a86b01..95be04c32c 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
+fun (pat : nat) '(x, y) => x + y = pat
+     : nat -> nat * nat -> Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 6fa357a90c..0bad472f41 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
 
 End Suboptimal.
+
+(** Test risk of collision for internal name *)
+Check fun pat => fun '(x,y) => x+y = pat.
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
index db2bbb0dc7..07a5bc0606 100644
--- a/test-suite/success/record_syntax.v
+++ b/test-suite/success/record_syntax.v
@@ -45,3 +45,11 @@ Record Foo := { foo : unit; }.
 Definition foo_ := {| foo := tt; |}.
 
 End E.
+
+Module F.
+
+Record Foo := { foo : nat * nat -> nat -> nat }.
+
+Definition foo_ := {| foo '(x,y) n := x+y+n |}.
+
+End F.