From b1a13bc7af4f4b8b5249712d0a982cc510a2cb85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 Jul 2016 15:47:10 +0200
Subject: Fixing use of "Declare Implicit Tactic" in refine.

---
 tactics/extratactics.ml4 | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 92d0ac983d..06fea367af 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -345,11 +345,18 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
+let constr_flags = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+  Pretyping.fail_evar = false;
+  Pretyping.expand_evars = true }
+
 let refine_tac simple {Glob_term.closure=closure;term=term} =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let flags = Pretyping.all_no_fail_flags in
+    let flags = constr_flags in
     let tycon = Pretyping.OfType concl in
     let lvar = { Pretyping.empty_lvar with
       Pretyping.ltac_constrs = closure.Glob_term.typed;
-- 
cgit v1.2.3