Define Tactics.bring_hyps in the new monad.

5 files changed, 16 insertions, 9 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 5d5b592ad4..bbbe62eb5d 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -162,7 +162,7 @@ let induction_trailer abs_i abs_j bargs =
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
 	  (tclTHENSEQ
-            [bring_hyps hyps; tclTRY (clear ids);
+            [Proofview.V82.of_tactic (bring_hyps hyps); tclTRY (clear ids);
 	     simple_elimination (mkVar id)]) gls
           end
           ))
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e2129ce535..498addf580 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -30,7 +30,6 @@ open Misctypes
 open Tacexpr
 open Proofview.Notations
 
-let bring_hyps hyps = Proofview.V82.tactic (bring_hyps hyps)
 let clear hyps = Proofview.V82.tactic (clear hyps)
 
 let collect_meta_variables c =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index ac56e6688b..724cea5b72 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -294,7 +294,7 @@ let lemInvIn id c ids =
       else
         (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids))
     in
-    ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c)))
+    ((Tacticals.New.tclTHEN (Tacticals.New.tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
         (intros_replace_ids)))
   end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aeac5e2642..8397521def 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -672,13 +672,21 @@ let apply_term hdc argl gl =
   refine (applist (hdc,argl)) gl
 
 let bring_hyps hyps =
-  if List.is_empty hyps then Refiner.tclIDTAC
+  if List.is_empty hyps then Tacticals.New.tclIDTAC
   else
-    (fun gl ->
-      let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
-      let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
+    Proofview.Goal.enter begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let concl = Proofview.Goal.concl gl in
+      let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
-      refine_no_check (mkApp (f, args)) gl)
+      let c = Goal.Refinable.make begin fun h ->
+        Goal.bind (Goal.Refinable.mkEvar h env newcl) begin fun ev ->
+          Goal.return (mkApp (ev, args))
+        end
+      end in
+      let c = Goal.bind c Goal.refine in
+      Proofview.tclSENSITIVE c
+    end
 
 let resolve_classes gl =
   let env = pf_env gl and evd = project gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 671343b128..e07518aba3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -172,7 +172,7 @@ val revert        : Id.t list -> tactic
 
 val apply_type : constr -> constr list -> tactic
 val apply_term : constr -> constr list -> tactic
-val bring_hyps : named_context -> tactic
+val bring_hyps : named_context -> unit Proofview.tactic
 
 val apply                 : constr -> tactic
 val eapply                : constr -> tactic