Fix printing of wit_constr and some ssr problems with printing empty lists

2 files changed, 17 insertions, 0 deletions

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.