diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_049.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_049.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_049.v b/test-suite/bugs/closed/HoTT_coq_049.v index 906ec329e0..31e7861de4 100644 --- a/test-suite/bugs/closed/HoTT_coq_049.v +++ b/test-suite/bugs/closed/HoTT_coq_049.v @@ -4,3 +4,4 @@ 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. *) +Abort. |