From 91eb9e8cd5c68d5a71c07787900a8bb6d0481ba9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Mar 2014 14:12:45 +0100
Subject: Lighter interface for creating refining tactics.

---
 proofs/proofview.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'proofs/proofview.ml')

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
-- 
cgit v1.2.3