Fixing side bug in db37c9f3f32ae7 delaying interpretation of the

right-hand side of a "change with": the rhs lives in the toplevel
environment.

1 files changed, 9 insertions, 0 deletions

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.