diff options
| author | Hugo Herbelin | 2018-09-29 13:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-10 20:30:39 +0200 |
| commit | 8abdd1f3d29f8fb0c47588869086cf5531dbc733 (patch) | |
| tree | e103dddd79cd1903cc3f74b60feafa690321e5b4 /test-suite/output/PrintModule.v | |
| parent | 040ad198e38776bb9f398329243b2fe41434f2d5 (diff) | |
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.
Diffstat (limited to 'test-suite/output/PrintModule.v')
| -rw-r--r-- | test-suite/output/PrintModule.v | 12 |
1 files changed, 12 insertions, 0 deletions
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. |