diff options
Diffstat (limited to 'test-suite/output/UnivBinders.v')
| -rw-r--r-- | test-suite/output/UnivBinders.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 266d94ad9..c6efc240a 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -44,6 +44,9 @@ Module mono. Monomorphic Definition monomono := Type@{MONOU}. Check monomono. + + Monomorphic Inductive monoind@{i} : Type@{i} := . + Monomorphic Record monorecord@{i} : Type@{i} := mkmonorecord {}. End mono. Check mono.monomono. (* qualified MONOU *) Import mono. |