From db28e827d21658797418c320d566fb99570b44b6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:20:35 +0200
Subject: Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions
 with evars)."

One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:

~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~

Thank you!
---
 pretyping/patternops.ml       | 4 +---
 test-suite/bugs/closed/5487.v | 9 ---------
 2 files changed, 1 insertion(+), 12 deletions(-)
 delete mode 100644 test-suite/bugs/closed/5487.v

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 75d3ed30ba..2090aad8a0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -160,9 +160,7 @@ 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.VarInstance _ ->
-        (* These are the two evar kinds used for existing goals *)
-        (* see Proofview.mark_in_evm *)
+      | Evar_kinds.GoalEvar -> 
 	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
deleted file mode 100644
index 9b995f4503..0000000000
--- a/test-suite/bugs/closed/5487.v
+++ /dev/null
@@ -1,9 +0,0 @@
-(* 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