1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 031cbc7c5..a1e57fd3c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -322,8 +322,6 @@ END
 (* Refine                                                             *)
 
 
-let refine_tac = Tactics.New.refine
-
 let refine_red_flags =
   Genredexpr.Lazy {
     Genredexpr.rBeta=true;
@@ -341,7 +339,10 @@ let refine_tac (ist, c) =
     let constrvars = Tacinterp.extract_ltac_constr_values ist env in
     let vars = (constrvars, ist.Geninterp.lfun) in
     let c = Goal.Refinable.make begin fun h ->
-      Goal.Refinable.constr_of_raw h true true vars c
+      Goal.bind Goal.concl (fun concl ->
+        let flags = Pretyping.all_no_fail_flags in
+        let tycon = Pretyping.OfType concl in
+        Goal.Refinable.constr_of_raw h tycon flags vars c)
     end in
     Proofview.Goal.lift c >>= fun c ->
     Proofview.tclSENSITIVE (Goal.refine c) <*>