From d1a39e06c44dc451d8a56a286017885d400ac435 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 6 May 2014 09:51:21 -0400 Subject: 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. --- test-suite/bugs/closed/HoTT_coq_049.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_049.v (limited to 'test-suite/bugs/closed/HoTT_coq_049.v') diff --git a/test-suite/bugs/closed/HoTT_coq_049.v b/test-suite/bugs/closed/HoTT_coq_049.v new file mode 100644 index 000000000..906ec329e --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_049.v @@ -0,0 +1,6 @@ +Require Import FunctionalExtensionality. + +Goal forall y, @f_equal = y. +intro. +apply functional_extensionality_dep. +(* Error: Ill-typed evar instance in HoTT/coq, Anomaly: Uncaught exception Reductionops.NotASort(_). Please report. before that. *) -- cgit v1.2.3