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.out | 8 ++++++++
 1 file changed, 8 insertions(+)

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

diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index 1a9bc068c5..7c7600b786 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -7,3 +7,11 @@ Module N : S with Module T := K := M
 Module N : S with Module T := M
 
 Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
+Module
+A
+:= Struct
+     Variant I : Set :=  C : nat -> I.
+     Record R : Set := Build_R { n : nat }.
+     Definition n : R -> nat.
+   End
+
-- 
cgit v1.2.3