From 064de6f6839c4ef963b83018812c5d4113eb2bb9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 30 Sep 2016 17:25:58 +0200
Subject: Fix bug #5045: [generalize] creates ill-typed terms in 8.6.

---
 test-suite/bugs/closed/5045.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/5045.v

(limited to 'test-suite/bugs/closed/5045.v')

diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v
new file mode 100644
index 000000000..dc38738d8
--- /dev/null
+++ b/test-suite/bugs/closed/5045.v
@@ -0,0 +1,3 @@
+Axiom silly : 1 = 1 -> nat -> nat.
+Goal forall pf : 1 = 1, silly pf 0 = 0 -> True.
+  Fail generalize (@eq nat).
-- 
cgit v1.2.3