From edb2b2535d62b37c324c98b28802c1b1699d4014 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 25 Nov 2017 22:08:01 +0100 Subject: Restrict universe context when declaring constants in obligations. --- test-suite/success/polymorphism.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test-suite') 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. -- cgit v1.2.3