diff options
Diffstat (limited to 'test-suite/success/polymorphism.v')
| -rw-r--r-- | test-suite/success/polymorphism.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index b3f9a4994..d76b30791 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -461,3 +461,10 @@ Section test_letin_subtyping. Qed. End test_letin_subtyping. + +Module ObligationRegression. + (** Test for a regression encountered when fixing obligations for + stronger restriction of universe context. *) + Require Import CMorphisms. + Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}. +End ObligationRegression. |