Lighter interface for creating refining tactics.

1 files changed, 24 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ae4b2e3363..0600a9c8ba 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -771,6 +771,9 @@ module V82 = struct
 
 end
 
+type goal = Goal.goal
+let build_goal = Goal.build
+let partial_solution = Goal.V82.partial_solution
 
 module Goal = struct
 
@@ -852,6 +855,27 @@ module Goal = struct
 
 end
 
+module Refine =
+struct
+  type handle = Evd.evar_map * goal list
+
+  let new_evar (evd, evs) env typ =
+    let (evd, ev) = Evarutil.new_evar evd env typ in
+    let (evk, _) = Term.destEvar ev in
+    let h = (evd, build_goal evk :: evs) in
+    (h, ev)
+
+  let refine f = Goal.raw_enter begin fun gl ->
+    let sigma = Goal.sigma gl in
+    let handle = (sigma, []) in
+    let ((sigma, evs), c) = f handle in
+    let sigma = partial_solution sigma gl.Goal.self c in
+    Proof.get >>= fun start ->
+    Proof.set { start with solution = sigma; comb = List.rev evs; }
+  end
+
+end
+
 module NonLogical = Proofview_monad.NonLogical
 
 let tclLIFT = Proofview_monad.Logical.lift