From 844b076bf5150a107d31cd4648955c3a6538a34b Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 28 Sep 2016 10:40:54 +0200
Subject: Fix #4762.

---
 tactics/eauto.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index cb206a7dd1..7e37722e93 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -291,7 +291,8 @@ module SearchProblem = struct
       in
       let rec_tacs =
 	let l =
-	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+          let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl)
 	in
 	List.map
 	  (fun (lgls, cost, pp) ->
-- 
cgit v1.2.3