diff options
Diffstat (limited to 'test-suite/prerequisite')
| -rw-r--r-- | test-suite/prerequisite/bind_univs.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v index f17c00e9d..e834fde11 100644 --- a/test-suite/prerequisite/bind_univs.v +++ b/test-suite/prerequisite/bind_univs.v @@ -3,3 +3,5 @@ Monomorphic Definition mono@{u} := Type@{u}. Polymorphic Definition poly@{u} := Type@{u}. + +Monomorphic Universe reqU. |