From e881720a724ffa4e6201cc1d460c66ce373713d9 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 13 Jan 2021 18:29:11 +0100
Subject: Make sure "Print Module" write a dot at the end of inductive
 definitions.

---
 test-suite/output/PrintModule.v | 7 +++++++
 1 file changed, 7 insertions(+)

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

diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 54ef305be4..b4de03b556 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -60,3 +60,10 @@ Print Func.
 End Shortest_path.
 
 End QUX.
+
+Module A.
+Variant I := C : nat -> I.
+Record R := { n : nat }.
+End A.
+
+Print Module A.
-- 
cgit v1.2.3