From 9324dcf528f16be420b08c376a6580c8987f50fd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Aug 2017 17:10:48 +0200
Subject: Using name given by user to name a 'pat, if any.

This works for contexts in Definition and co, but not yet for "fun" and co.
---
 test-suite/output/PatternsInBinders.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite/output/PatternsInBinders.v')

diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0bad472f41..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -67,3 +67,8 @@ End Suboptimal.
 
 (** Test risk of collision for internal name *)
 Check fun pat => fun '(x,y) => x+y = pat.
+
+(** Test name in degenerate case *)
+Definition f 'x := x+x.
+Print f.
+Check fun 'x => x+x.
-- 
cgit v1.2.3