From 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Apr 2017 16:30:45 +0200
Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with
 evars).

The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.

One day, evar kinds will need a little cleaning...
---
 pretyping/patternops.ml       | 4 +++-
 test-suite/bugs/closed/5487.v | 9 +++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5487.v

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 2090aad8a0..75d3ed30ba 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -160,7 +160,9 @@ let pattern_of_constr env sigma t =
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
 	let () = ignore (pattern_of_constr env ty) in
         assert (not b); PMeta (Some id)
-      | Evar_kinds.GoalEvar -> 
+      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
+        (* These are the two evar kinds used for existing goals *)
+        (* see Proofview.mark_in_evm *)
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v
new file mode 100644
index 0000000000..9b995f4503
--- /dev/null
+++ b/test-suite/bugs/closed/5487.v
@@ -0,0 +1,9 @@
+(* Was a collision between an ltac pattern variable and an evar *)
+
+Goal forall n, exists m, n = m :> nat.
+Proof.
+  eexists.
+  Fail match goal with
+  | [ |- ?x = ?y ]
+    => match x with y => idtac end
+  end.
-- 
cgit v1.2.3