From 9a82982c1eb8cb1d6a61d3d497d669591fb68747 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 3 Oct 2014 15:21:05 +0200
Subject: Fixing #3657 (check that both sides of a "change with" have the same
 type, what is necessary condition to ensure that the conversion of bodies
 will not raise an anomaly).

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

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

diff --git a/test-suite/bugs/closed/3657.v b/test-suite/bugs/closed/3657.v
new file mode 100644
index 000000000..778fdab19
--- /dev/null
+++ b/test-suite/bugs/closed/3657.v
@@ -0,0 +1,12 @@
+(* Check typing of replaced objects in change - even though the failure
+   was already a proper error message (but with a helpless content) *)
+
+Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
+Arguments bar {_} _ {_}.
+Instance: forall A a, @foo A a.
+intros; constructor.
+abstract reflexivity.
+Defined.
+Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
+Proof.
+  Fail change (bar (fun _ : Set => Set)) with (bar Set).
-- 
cgit v1.2.3