diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-21 00:53:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | 765392492df2f5e065b2b5e706b6620846337cc0 (patch) | |
| tree | ccf14d9040e76acca2a902cdefa57fefc53bc64a /test-suite/output/UnivBinders.v | |
| parent | 280c922fc55b57c430cad721c83650a796a375fd (diff) | |
Universe binders survive sections, modules and compilation.
Diffstat (limited to 'test-suite/output/UnivBinders.v')
| -rw-r--r-- | test-suite/output/UnivBinders.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 46904b384..f0a990986 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -52,3 +52,30 @@ Fail Print mono@{E}. (* Not everything can be printed with custom universe names. *) Fail Print Coq.Init.Logic@{E}. + +(* Universe binders survive through compilation, sections and modules. *) +Require bind_univs. +Print bind_univs.mono. +Print bind_univs.poly. + +Section SomeSec. + Universe u. + Definition insec@{v} := Type@{u} -> Type@{v}. + Print insec. +End SomeSec. +Print insec. + +Module SomeMod. + Definition inmod@{u} := Type@{u}. + Print inmod. +End SomeMod. +Print SomeMod.inmod. +Import SomeMod. +Print inmod. + +Module Type SomeTyp. Definition inmod := Type. End SomeTyp. +Module SomeFunct (In : SomeTyp). + Definition infunct@{u v} := In.inmod@{u} -> Type@{v}. +End SomeFunct. +Module Applied := SomeFunct(SomeMod). +Print Applied.infunct. |