2 files changed, 42 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
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 409bbb76a1..436511f4a9 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -376,6 +376,24 @@ module Goal : sig
   val refresh_sigma : 'a t -> 'a t tactic
 end
 
+(** A light interface for building tactics out of partial term. It should be
+    easier to use than the {!Goal} one. *)
+module Refine : sig
+
+  type handle
+  (** A handle to thread along in state-passing style. *)
+
+  val new_evar : handle -> Environ.env -> Constr.types -> handle * Constr.t
+  (** Create a new hole that will be added to the goals to solve. *)
+
+  val refine : (handle -> handle * Constr.t) -> unit tactic
+  (** Given a term with holes that have been generated through {!new_evar}, this
+      function fills the current hole with the given constr and creates goals
+      for all the holes in their generation order. Exceptions raised by the
+      function are caught. *)
+
+end
+
 (* The [NonLogical] module allows to execute side effects in tactics
    (non-logical side-effects are not discarded at failures). *)
 module NonLogical : sig