Tentative workaround for bug #3798.

Ultimately setoid rewrite should be written in the monad to fix it properly.

2 files changed, 43 insertions, 0 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fdc93bcb90..d1b6afe220 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -156,6 +156,41 @@ let build_by_tactic env ctx ?(poly=false) typ tac =
   assert(Univ.ContextSet.is_empty ctx);
   cb, status, univs
 
+let refine_by_tactic env sigma ty tac =
+  (** Save the initial side-effects to restore them afterwards. We set the
+      current set of side-effects to be empty so that we can retrieve the
+      ones created during the tactic invocation easily. *)
+  let eff = Evd.eval_side_effects sigma in
+  let sigma = Evd.drop_side_effects sigma in
+  (** Start a proof *)
+  let prf = Proof.start sigma [env, ty] in
+  let (prf, _) =
+    try Proof.run_tactic env tac prf
+    with Logic_monad.TacticFailure e as src ->
+      (** Catch the inner error of the monad tactic *)
+      let (_, info) = Errors.push src in
+      iraise (e, info)
+  in
+  (** Plug back the retrieved sigma *)
+  let sigma = Proof.in_proof prf (fun sigma -> sigma) in
+  let ans = match Proof.initial_goals prf with
+  | [c, _] -> c
+  | _ -> assert false
+  in
+  let ans = Reductionops.nf_evar sigma ans in
+  (** [neff] contains the freshly generated side-effects *)
+  let neff = Evd.eval_side_effects sigma in
+  (** Reset the old side-effects *)
+  let sigma = Evd.drop_side_effects sigma in
+  let sigma = Evd.emit_side_effects eff sigma in
+  (** Get rid of the fresh side-effects by internalizing them in the term
+      itself. Note that this is unsound, because the tactic may have solved
+      other goals that were already present during its invocation, so that
+      those goals rely on effects that are not present anymore. Hopefully,
+      this hack will work in most cases. *)
+  let ans = Term_typing.handle_side_effects env ans neff in
+  ans, sigma
+
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
    resolution by application of tactics *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index edbc18a366..5e0fb4dd36 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -157,6 +157,14 @@ val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
+val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+  constr * Evd.evar_map
+(** A variant of the above function that handles open terms as well.
+    Caveat: all effects are purged in the returned term at the end, but other
+    evars solved by side-effects are NOT purged, so that unexpected failures may
+    occur. Ideally all code using this function should be rewritten in the
+    monad. *)
+
 (** Declare the default tactic to fill implicit arguments *)
 
 val declare_implicit_tactic : unit Proofview.tactic -> unit