From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/HoTT_coq_059.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_059.v (limited to 'test-suite/bugs/closed/HoTT_coq_059.v') diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v new file mode 100644 index 00000000..9c7e394d --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_059.v @@ -0,0 +1,17 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +Set Universe Polymorphism. + +Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x. +Notation "a = b" := (eq a b) : type_scope. + +Section foo. + Class Funext := { path_forall :> forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }. + Context `{Funext, Funext}. + + Set Printing Universes. + + (** Typeclass resolution should pick up the different instances of Funext automatically *) + Definition foo := (@path_forall _ _ _ (@path_forall _ Set)). + (* Toplevel input, characters 0-60: +Error: Universe inconsistency (cannot enforce Top.24 <= Top.23 because Top.23 +< Top.22 <= Top.24). *) -- cgit v1.2.3