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 c6efc240a6..c6a6b8231f 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -30,6 +30,9 @@ Unset Strict Universe Declaration. order of appearance. *) Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. Print foo. + +Check Type@{i} -> Type@{j}. + Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) |