From 80d36bc6538b7feaab3dfa43f6e234ae85b55692 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 07:27:06 +0100
Subject: A test checking for non-collision of name in irrefutable patterns.

---
 test-suite/output/PatternsInBinders.out | 2 ++
 test-suite/output/PatternsInBinders.v   | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'test-suite/output')

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.
-- 
cgit v1.2.3