Tentative workaround for bug #3798.

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

4 files changed, 45 insertions, 36 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fdc93bcb9..d1b6afe22 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 edbc18a36..5e0fb4dd3 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
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a3914da15..0140f74f5 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -629,11 +629,9 @@ let solve_remaining_by env sigma holes by =
       | None -> sigma
         (** Evar should not be defined, but just in case *)
       | Some evi ->
-        let ctx = Evd.evar_universe_context sigma in
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
-        let c, _, ctx = Pfedit.build_by_tactic env ctx ty solve_tac in
-        let sigma = Evd.set_universe_context sigma ctx in
+        let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
         Evd.define evk c sigma
     in
     List.fold_left solve sigma indep
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 23de47d56..b1ff0e401 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2349,39 +2349,7 @@ let _ =
     if has_type arg (glbwit wit_tactic) then
       let tac = out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
-      (** 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
+      Pfedit.refine_by_tactic env sigma ty tac
     else
       failwith "not a tactic"
   in