aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_059.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-05-06 09:51:21 -0400
committerGravatar Jason Gross <jgross@mit.edu>2014-05-06 16:11:43 -0400
commitd1a39e06c44dc451d8a56a286017885d400ac435 (patch)
treef83237ecf03b9d809d888ea31a842e6fb6d716d0 /test-suite/bugs/closed/HoTT_coq_059.v
parentd40091c015b68cc1a8403ca5dcc74323bf939f37 (diff)
Add regression tests for univ. poly. and prim proj
These regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently passes. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_059.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_059.v17
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 000000000..9c7e394dc
--- /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). *)