diff options
Diffstat (limited to 'test-suite/output/UnivBinders.v')
| -rw-r--r-- | test-suite/output/UnivBinders.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 013f215b5..a65a1fdf3 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -56,6 +56,10 @@ Fail Print mono@{E}. (* Not everything can be printed with custom universe names. *) Fail Print Coq.Init.Logic@{E}. +(* Nice error when constraints are impossible. *) +Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. +Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. + (* Universe binders survive through compilation, sections and modules. *) Require bind_univs. Print bind_univs.mono. |