From 4c576db3ed40328caa37144eb228365f497293e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Nov 2014 22:13:28 +0100
Subject: Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
 right-hand side of a "change with": the rhs lives in the toplevel
 environment.

---
 test-suite/success/change.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index cd2dd77f9e..1f0b7d38a9 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -50,3 +50,12 @@ Abort.
 Goal nat = nat :> Set.
 Fail change nat with (@id Type nat). (* would otherwise be ill-typed *)
 Abort.
+
+(* Check typing env for rhs is the correct one *)
+
+Goal forall n, let x := n in id (fun n => n + x) 0 = 0.
+intros.
+unfold x.
+(* check that n in 0+n is not interpreted as the n from "fun n" *)
+change n with (0+n).
+Abort.
-- 
cgit v1.2.3