Generalizing the refine primitive so as to accept tactic arguments.

2 files changed, 23 insertions, 5 deletions

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1ee6e0ca5..c96a2e50a 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -70,8 +70,7 @@ let add_side_effect env = function
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
-let make_refine_enter ?(unsafe = true) f =
-  { enter = fun gl ->
+let generic_refine ?(unsafe = true) f gl =
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
@@ -82,7 +81,10 @@ let make_refine_enter ?(unsafe = true) f =
   let prev_future_goals = Evd.future_goals sigma in
   let prev_principal_goal = Evd.principal_future_goal sigma in
   (** Create the refinement term *)
-  let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+  Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+  f >>= fun (v, c) ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
   let evs = Evd.future_goals sigma in
   let evkmain = Evd.principal_future_goal sigma in
   (** Redo the effects in sigma in the monad's env *)
@@ -122,7 +124,18 @@ let make_refine_enter ?(unsafe = true) f =
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
   Proofview.tclUNIT v
-  }
+  end
+
+let lift c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+  let Sigma (c, sigma, _) = c.run (Sigma.Unsafe.of_evar_map sigma) in
+  Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () ->
+  Proofview.tclUNIT c
+  end
+
+let make_refine_enter ?unsafe f =
+  { enter = fun gl -> generic_refine ?unsafe (lift f) gl }
 
 let refine_one ?(unsafe = true) f =
   Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1a254d578..1dcee3188 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -12,6 +12,7 @@
     in Ltac which is actually based on the one below. *)
 
 open Proofview
+open Proofview.Notations
 
 (** {6 The refine tactic} *)
 
@@ -31,7 +32,11 @@ val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
     type-checked beforehand. *)
 
 val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
-(** A generalization of [refine] which assumes exactly one goal under focus *)
+(** A variant of [refine] which assumes exactly one goal under focus *)
+
+val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
+  ([ `NF ], 'r) Proofview.Goal.t -> 'a tactic
+(** The general version of refine. *)
 
 (** {7 Helper functions} *)