From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/success/change.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'test-suite/success/change.v') diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 1f0b7d38..a9821b02 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -59,3 +59,12 @@ unfold x. (* check that n in 0+n is not interpreted as the n from "fun n" *) change n with (0+n). Abort. + +(* Check non-collision of non-normalized defined evars with pattern variables *) + +Goal exists x, 1=1 -> x=1/\x=1. +eexists ?[n]; intros; split. +eassumption. +match goal with |- ?x=1 => change (x=1) with (0+x=1) end. +match goal with |- 0+1=1 => trivial end. +Qed. -- cgit v1.2.3