From 8abdd1f3d29f8fb0c47588869086cf5531dbc733 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 29 Sep 2018 13:25:15 +0200
Subject: Miscellaneous refinements/cleaning of module printing.

This refines the fix to #2169 by distinguishing the short and
non-short printing modes.

This prepares functionalization of printers by always passing env
rather than setting env to None in short mode. This is not strictly
necessary for the env which is not used for printing global references
but it shall be more consistent in style when passing e.g. the nametab
functionally.

We however keep the fallback printer used in case of error while
printing: due to missing registration of submodule fields in the
nametab, printing with types does not work if there are references to
an inner module.
---
 test-suite/output/PrintModule.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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

diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 5f30f7cda6..54ef305be4 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -1,3 +1,5 @@
+(* Bug #2169 *)
+
 Module FOO.
 
 Module M.
@@ -12,6 +14,10 @@ Module N : S with Definition T := nat := M.
 
 Print Module N.
 
+Set Short Module Printing.
+Print Module N.
+Unset Short Module Printing.
+
 End FOO.
 
 Module BAR.
@@ -31,8 +37,14 @@ Module N : S with Module T := K := M.
 
 Print Module N.
 
+Set Short Module Printing.
+Print Module N.
+Unset Short Module Printing.
+
 End BAR.
 
+(* Bug #4661 *)
+
 Module QUX.
 
 Module Type Test.
-- 
cgit v1.2.3