Lighter interface for creating refining tactics.

1 files changed, 18 insertions, 0 deletions

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