Merge branch 'v8.5' into trunk.

3 files changed, 2 insertions, 51 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a3914da153..0140f74f50 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 23de47d567..b1ff0e4014 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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1f1248d7c..07969c7d74 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,22 +59,7 @@ let dloc = Loc.ghost
 
 let typ_of = Retyping.get_type_of
 
-(* Option for 8.4 compatibility *)
 open Goptions
-let legacy_elim_if_not_fully_applied_argument = ref false
-
-let use_legacy_elim_if_not_fully_applied_argument () =
-  !legacy_elim_if_not_fully_applied_argument
-  || Flags.version_less_or_equal Flags.V8_4
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "partially applied elimination argument legacy";
-      optkey   = ["Legacy";"Partially";"Applied";"Elimination";"Argument"];
-      optread  = (fun () -> !legacy_elim_if_not_fully_applied_argument) ;
-      optwrite = (fun b -> legacy_elim_if_not_fully_applied_argument := b) }
 
 (* Option for 8.2 compatibility *)
 let dependent_propositions_elimination = ref true