diff options
| author | Guillaume Melquiond | 2021-01-13 18:29:11 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-13 21:03:41 +0100 |
| commit | e881720a724ffa4e6201cc1d460c66ce373713d9 (patch) | |
| tree | e9e70f031996d23609f5d8ef5fd1b381646189fd /test-suite/output/PrintModule.v | |
| parent | 9fef12aadf0e7afea3d89a00cb7216b2b008cf5c (diff) | |
Make sure "Print Module" write a dot at the end of inductive definitions.
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. |