diff options
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. |