diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
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) -> |