Fixing an extra bug with pattern_of_constr.

Ensure in type constr_pattern that those preexisting existential
variables of the goal which do not contribute as pattern variables are
expanded: constr_pattern is not observed up to evar expansion (like
EConstr does), so we need to pre-normalize defined evars in patterns
to that matching against an EConstr works.

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 1f0b7d38a..a9821b027 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.