From 1280a492b87f02aac8c8f8496ebd42039762d7e4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Oct 2020 15:13:15 +0200
Subject: Fix printing for empty primitive arrays

Fix #13178
---
 test-suite/bugs/closed/bug_13178.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13178.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13178.v b/test-suite/bugs/closed/bug_13178.v
new file mode 100644
index 0000000000..d9c516c362
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13178.v
@@ -0,0 +1,3 @@
+Primitive array := #array_type.
+
+Check [| | 0 |].
-- 
cgit v1.2.3


From 225a4ee2871b58661f9689255237a1e189ee6a4c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 2 Nov 2020 15:03:09 +0100
Subject: Nicer spacing when printing array literals

From

    [|x; y; z | def : ty |]

to

    [| x; y; z | def : ty |]
---
 test-suite/output/prim_array.out |  9 +++++++++
 test-suite/output/prim_array.v   | 10 ++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 test-suite/output/prim_array.out
 create mode 100644 test-suite/output/prim_array.v

(limited to 'test-suite')

diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out
new file mode 100644
index 0000000000..6c12153ab9
--- /dev/null
+++ b/test-suite/output/prim_array.out
@@ -0,0 +1,9 @@
+[| | 0 : nat |]
+     : array nat
+[| 1; 2; 3 | 0 : nat |]
+     : array nat
+[| | 0 : nat |]@{Set}
+     : array@{Set} nat
+[| bool; list nat | nat : Set |]@{prim_array.4}
+     : array@{prim_array.4} Set
+(* {prim_array.4} |= Set < prim_array.4 *)
diff --git a/test-suite/output/prim_array.v b/test-suite/output/prim_array.v
new file mode 100644
index 0000000000..a82f6a16f1
--- /dev/null
+++ b/test-suite/output/prim_array.v
@@ -0,0 +1,10 @@
+Primitive array := #array_type.
+
+Check [| | 0 |].
+
+Check [| 1; 2; 3 | 0 |].
+
+Set Printing Universes.
+Check [| | 0 |].
+
+Check [| bool; list nat | nat |].
-- 
cgit v1.2.3