New primitive allowing to modify refine handles.

2 files changed, 14 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 08a4d41c9..f1759548e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -993,6 +993,14 @@ struct
     refine f
   end
 
+  let update (evd, gls) f =
+    let nevd, ans = f evd in
+    let fold ev _ accu =
+      if not (Evd.mem evd ev) then build_goal ev :: accu else accu
+    in
+    let gls = Evd.fold_undefined fold nevd gls in
+    (nevd, gls), ans
+
 end
 
 module NonLogical = Proofview_monad.NonLogical
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 1ed5d92ad..288a46cb7 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -437,6 +437,12 @@ module Refine : sig
   val with_type : handle -> Environ.env -> Term.constr -> Term.types -> handle*Term.constr
   (** [with_type h env c t] coerces refinable term [c] to type [t]. *)
 
+  val update : handle -> (Evd.evar_map -> Evd.evar_map * 'a) -> handle * 'a
+  (** [update h f] update the handle by applying [f] to the underlying evar map.
+      The [f] function must be monotonous, that is, for any evar map [evd],
+      [fst (f evd)] should be an extension of [evd]. New evars generated by [f]
+      are turned into goals. Use with care. *)
+
   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