diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_059.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_059.v | 17 |
1 files changed, 17 insertions, 0 deletions
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). *) |