From 6058cdf5e70822e4501c61dfd969e4746c01145b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 8 Jan 2014 09:06:58 +0100
Subject: Exporting the full pretyper options in Goal.constr_of_raw.

---
 tactics/extratactics.ml4 | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 031cbc7c5d..a1e57fd3c4 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) <*>
-- 
cgit v1.2.3