diff options
| author | coqbot-app[bot] | 2021-01-20 12:10:46 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-20 12:10:46 +0000 |
| commit | 471fc4035adec0e96957aaddbd7fd3034539dc22 (patch) | |
| tree | f7bc0de59394bac0bf528d2cf8a40cd50262dbd9 /test-suite/output/PrintModule.v | |
| parent | 071c50e9c2755e93766e5fb047b0a9065934e8fe (diff) | |
| parent | e881720a724ffa4e6201cc1d460c66ce373713d9 (diff) | |
Merge PR #13744: Make sure "Print Module" write a dot at the end of inductive definitions.
Reviewed-by: SkySkimmer
Diffstat (limited to 'test-suite/output/PrintModule.v')
| -rw-r--r-- | test-suite/output/PrintModule.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |