From 67089b35889648196c1e7b378f77d368de0105a9 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Thu, 22 Oct 2020 03:25:15 +0200
Subject: Fix printing of wit_constr and some ssr problems with printing empty
 lists

---
 test-suite/output/bug_13238.out |  4 ++++
 test-suite/output/bug_13238.v   | 13 +++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 test-suite/output/bug_13238.out
 create mode 100644 test-suite/output/bug_13238.v

(limited to 'test-suite')

diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out
new file mode 100644
index 0000000000..bda21aa9e3
--- /dev/null
+++ b/test-suite/output/bug_13238.out
@@ -0,0 +1,4 @@
+Ltac bug_13238.t1 x := replace (x x) with (x x)
+Ltac bug_13238.t2 x := case : x 
+Ltac bug_13238.t3 := by move ->
+Ltac bug_13238.t4 := congr True 
diff --git a/test-suite/output/bug_13238.v b/test-suite/output/bug_13238.v
new file mode 100644
index 0000000000..9b8063bf13
--- /dev/null
+++ b/test-suite/output/bug_13238.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Ltac t1 x := replace (x x) with (x x).
+Print t1.
+
+Ltac t2 x := case: x.
+Print t2.
+
+Ltac t3 := by move->.
+Print t3.
+
+Ltac t4 := congr True.
+Print t4.
-- 
cgit v1.2.3