From 495bccc436cfe72af9955b4b9d8564a8831850b9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 23:23:53 +0100
Subject: Fixing #4499 (not using unnamed record field in {| |} notation).

---
 test-suite/output/Record.out | 6 ++++++
 test-suite/output/Record.v   | 5 +++++
 2 files changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 36d643a447..37b4fb25f7 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -14,3 +14,9 @@ build 5
      : test_r
 build_c 5
      : test_c
+fun '(C _ p) => p
+     : N -> True
+fun '{| T := T |} => T
+     : N -> Type
+fun '(C T p) => (T, p)
+     : N -> Type * True
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 6aa3df9830..c3d9f1e573 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -19,3 +19,8 @@ Check build 5.
 Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
+
+Record N := C { T : Type; _ : True }.
+Check fun x:N => let 'C _ p := x in p.
+Check fun x:N => let 'C T _ := x in T.
+Check fun x:N => let 'C T p := x in (T,p).
-- 
cgit v1.2.3