Merge branch 'v8.5' into trunk.

17 files changed, 193 insertions, 138 deletions

diff --git a/CHANGES b/CHANGES
index 3471bc61c..a8411a212 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,15 +14,14 @@ Logic
   parameters, i.e. [@p] is definitionally equal to [λ params r. r.(p)].
   Records with primitive projections have eta-conversion, the
   canonical form being [mkR pars (p1 t) ... (pn t)].
-
 - New universe polymorphism (see reference manual)
 - New option -type-in-type to collapse the universe hierarchy (this makes the
   logic inconsistent).
-- The guard condition for fixpoints is now a bit stricter. Propagation of
-subterm value through pattern matching is restricted according to the return
-predicate. Restores compatibility of Coq's logic with the propositional
-extensionality axiom. May create incompatibilities in recursive programs heavily
-using dependent types.
+- The guard condition for fixpoints is now a bit stricter. Propagation
+  of subterm value through pattern matching is restricted according to
+  the return predicate. Restores compatibility of Coq's logic with the
+  propositional extensionality axiom. May create incompatibilities in
+  recursive programs heavily using dependent types.
 
 Vernacular commands
 
@@ -44,7 +43,7 @@ Vernacular commands
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
   is deprecated.
-- "Search" "About" "SearchHead" "SearchRewrite" and "SearchPattern"
+- "Search", "About", "SearchHead", "SearchRewrite" and "SearchPattern"
   now search for hypothesis (of the current goal by default) first.
   They now also support the goal selector prefix to specify another
   goal to search: e.g. "n:Search id". This is also true for
@@ -63,13 +62,13 @@ Vernacular commands
 - New "Refine Instance Mode" option that allows to deactivate the generation of
   obligations in incomplete typeclass instances, raising an error instead.
 - "Collection" command to name sets of section hypotheses.  Named collections
-  can be used in the syntax of "Proof using" to assert with section variables
+  can be used in the syntax of "Proof using" to assert which section variables
   are used in a proof.
 - The "Optimize Proof" command can be placed in the middle of a proof to
-  force the compaction the data structure used to represent the ongoing
-  proof (evar map).  This may result in a lower memory footprint and speed up
+  force the compaction of the data structure used to represent the ongoing
+  proof (evar map). This may result in a lower memory footprint and speed up
   the execution of the following tactics.
-- "Optimize Heap" command to tell the OCaml runtime to performa a major
+- "Optimize Heap" command to tell the OCaml runtime to perform a major
   garbage collection step and heap compaction.
 
 Specification Language
@@ -98,9 +97,9 @@ Tactics
   instantiation information of existential variables is always
   propagated to tactics, removing the need to manually use the
   "instantiate" tactics to mark propagation points.
-  * New tactical (a+b) insert a backtracking point. When (a+b);c fails
+  * New tactical (a+b) inserts a backtracking point. When (a+b);c fails
     during the execution of c, it can backtrack and try b instead of a.
-  * New tactical (once a) removes all the backtracking point from a
+  * New tactical (once a) removes all the backtracking points from a
     (i.e. it selects the first success of a).
   * Tactic "constructor" is now fully backtracking, thus deprecating
     the need of the undocumented "constructor <tac>" syntax which is
@@ -109,27 +108,27 @@ Tactics
   * New "multimatch" variant of "match" tactic which backtracks to
     new branches in case of a later failure. The "match" tactic is
     equivalent to "once multimatch".
-  * New selector all: to qualify a tactic allows applying a tactic to
-    all the focused goal, instead of just the first one as is the
+  * New selector "all:" such that "all:tac" applies tactic "tac" to
+    all the focused goals, instead of just the first one as is the
     default.
   * A corresponding new option Set Default Goal Selector "all" makes
     the tactics in scripts be applied to all the focused goal by default
-  * New selector par: to qualify a tactic allows applying a (terminating)
-    tactic to all the focused goal in parallel.  The number of worker can
-    be selected with -async-proofs-tac-j and also limited using the
+  * New selector "par:" such that "par:tac" applies the (terminating)
+    tactic "tac" to all the focused goal in parallel. The number of worker
+    can be selected with -async-proofs-tac-j and also limited using the
     coqworkmgr utility.
   * New tactics "revgoals", "cycle" and "swap" to reorder goals.
-  * The semantics of recursive tactics (introduced with Ltac t :=
-    ... or let rec t := ... in ...) changes slightly as t is now
-    applied to every goal not each goal independently, in particular
-    it may be applied when no goal are left. This may cause tactics
-    such as let rec t := constructor;t to loop indefinitely. The
-    simple fix is to rewrite the recursive calls as follows: let rec t
-    := constructor;[t..] which recovers the earlier behavior (source
-    of rare incompatibilities).
-  * New tactic language feature "numgoals" to count number of goals.
-    Accompanied by "guard" tactic which fails if a Boolean test does
-    not pass.
+  * The semantics of recursive tactics (introduced with "Ltac t := ..."
+    or "let rec t := ... in ...") changed slightly as t is now
+    applied to every goal, not each goal independently. In particular
+    it may be applied when no goals are left. This may cause tactics
+    such as "let rec t := constructor;t" to loop indefinitely. The
+    simple fix is to rewrite the recursive calls as follows:
+    "let rec t := constructor;[t..]" which recovers the earlier behavior
+    (source of rare incompatibilities).
+  * New tactic language feature "numgoals" to count number of goals. It is
+    accompanied by a "guard" tactic which fails if a Boolean test over
+    integers does not pass.
   * New tactical "[> ... ]" to apply tactics to individual goals.
   * New tactic "gfail" which works like "fail" except it will also
     fail if every goal has been solved.
@@ -143,7 +142,7 @@ Tactics
     Unshelve command.
   * A variant shelve_unifiable only removes those goals which appear
     as existential variables in other goals. To emulate the old
-    refine, use (refine c;shelve_unifiable). This can still cause
+    refine, use "refine c;shelve_unifiable". This can still cause
     incompatibilities in rare occasions.
   * New "give_up" tactic to skip over a goal without admitting it.
 - Matching using "lazymatch" was fundamentally modified. It now behaves
@@ -164,7 +163,9 @@ Tactics
   opposite side, new tactic "dtauto" is able to destruct any
   record-like inductive types, superseding the old version of "tauto".
 - Similarly, "intuition" has been made more uniform and, where it now
-  fails, "dintuition" can be used. (possible source of incompatibilities)
+  fails, "dintuition" can be used (possible source of incompatibilities).
+- New option "Unset Intuition Negation Unfolding" for deactivating automatic
+  unfolding of "not" in intuition.
 - Tactic notations can now be defined locally to a module (use "Local" prefix).
 - Tactic "red" now reduces head beta-iota redexes (potential source of
   rare incompatibilities).
@@ -221,15 +222,15 @@ Tactics
   the relevant hypotheses).
 - New construct "uconstr:c" and "type_term c" to build untyped terms.
 - Binders in terms defined in Ltac (either "constr" or "uconstr") can
-  now take their names from identifier defined in Ltac. As a
-  consequence, a name cannot be used in a binder (constr:(fun x =>
-  ...)) if an Ltac variable of that name already exists and does not
+  now take their names from identifiers defined in Ltac. As a
+  consequence, a name cannot be used in a binder "constr:(fun x =>
+  ...)" if an Ltac variable of that name already exists and does not
   contain an identifier. Source of occasional incompatibilities.
 - The "refine" tactic now accepts untyped terms built with "uconstr"
   so that terms with holes can be constructed piecewise in Ltac.
 - New bullets --, ++, **, ---, +++, ***, ... made available.
 - More informative messages when wrong bullet is used.
-- bullet suggestion when a subgoal is solved.
+- Bullet suggestion when a subgoal is solved.
 - New tactic "enough", symmetric to "assert", but with subgoals
   swapped, as a more friendly replacement of "cut".
 - In destruct/induction, experimental modifier "!" prefixing the
@@ -270,9 +271,9 @@ Notations
   (possible source of incompatibilities)
 - Notations accept term-providing tactics using the $(...)$ syntax.
 - "Bind Scope" can no longer bind "Funclass" and "Sortclass".
-- A notation can be given a (compat "8.x") annotation, making
-  it behave like a (only parsing), but flags may active warning
-  or error when this notation is used.
+- A notation can be given a (compat "8.x") annotation, making it behave
+  like a "only parsing" notation, but the annotation may lead to eventually
+  issue warnings or errors in further versions when this notation is used.
 - More systematic insertion of spaces as a default for printing
   notations ("format" still available to override the default).
 - In notations, a level modifier referring to a non-existent variable is
@@ -305,14 +306,14 @@ Interfaces
 - CoqIDE supports asynchronous edition of the document, ongoing tasks and
   errors are reported in the bottom right window.  The number of workers
   taking care of processing proofs can be selected with -async-proofs-j.
-- CoqIDE highlight in yellow "unsafe" commands such as axiom
+- CoqIDE highlights in yellow "unsafe" commands such as axiom
   declarations, and tactics like "admit".
 - CoqIDE supports Proof General like key bindings;
   to activate the PG mode go to Edit -> Preferences -> Editor.
   For the documentation see Help -> Help for PG mode.
 - CoqIDE automatically retracts the locked area when one edits the
   locked text.
-- CoqIDE search and replace got regular expressions power.  See the
+- CoqIDE search and replace got regular expressions power. See the
   documentation of OCaml's Str module for the supported syntax.
 - Many CoqIDE windows, including the query one, are now detachable to
   improve usability on multi screen work stations.
@@ -334,7 +335,7 @@ Internal Infrastructure
   initially does a "Require" of Prelude.vo (or nothing when given
   the options -noinit or -nois).
 - The format of vo files has slightly changed: cf final comments in
-  checker/cic.mli
+  checker/cic.mli.
 - The build system does not produce anymore programs named coqtop.opt
   and a symbolic link to coqtop. Instead, coqtop is now directly
   an executable compiled with the best OCaml compiler available.
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index 28a6f6903..c8e36197c 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -306,8 +306,8 @@ canonical structures.
 We need some infrastructure for that.
 
 \begin{coq_example}
+Require Import Strings.String.
 Module infrastructure.
-  Require Import Strings.String.
   Inductive phantom {T : Type} (t : T) : Type := Phantom.
   Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2.
   Definition id {T} {t : T} (x : phantom t) := x.
@@ -318,8 +318,8 @@ Module infrastructure.
 End infrastructure.
 \end{coq_example}
 
-To explain the notation $[find v | t1 \textasciitilde t2]$ lets pick one
-of its instances: $[find e  | EQ.obj e \textasciitilde T | "is not an EQ.type" ]$.
+To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one
+of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}.
 It should be read as: ``find a class e such that its objects have type T
 or fail with message "T is not an EQ.type"''.
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 2a976a07b..193479cce 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1929,30 +1929,60 @@ tools. The format is unspecified if {\str} doesn't end in
 \texttt{.dot} or \texttt{.gv}.
 
 \section[Existential variables]{Existential variables\label{ExistentialVariables}}
+\label{evars}
 
-Coq terms can include existential variables. An existential variable
-is a placeholder intended to eventually be replaced by an actual
-subterm though which subterm it will be replaced by is still unknown.
+Coq terms can include existential variables which
+represents unknown subterms to eventually be replaced by actual
+subterms.
 
 Existential variables are generated in place of unsolvable implicit
-arguments when using commands such as \texttt{Check} (see
-Section~\ref{Check}) or in place of unsolvable instances when using
-tactics such as \texttt{eapply} (see Section~\ref{eapply}). They can
-only appear as the result of a command displaying a term and they are
-represented by ``?'' followed by a number. They cannot be entered by
-the user (though they can be generated from ``\_'' when the
-corresponding implicit argument is unsolvable).
-
-A given existential variable name can occur several times in a term
-meaning the corresponding expected instance is shared. Each
-existential variable is relative to a context, as shown by {\tt Show
-  Existential} when in the process of proving a goal (see
-Section~\ref{ShowExistentials}). Henceforth, each occurrence of an
-existential variable in a term is subject to an instance of the
-variables of its context of definition which is specific to this
-occurrence.
+arguments or ``{\tt \_}'' placeholders when using commands such as
+\texttt{Check} (see Section~\ref{Check}) or when using tactics such as
+\texttt{refine}~(see Section~\ref{refine}), as well as in place of unsolvable
+instances when using tactics such that \texttt{eapply} (see
+Section~\ref{eapply}). An existential variable is defined in a
+context, which is the context of variables of the placeholder which
+generated the existential variable, and a type, which is the expected
+type of the placeholder. 
+
+As a consequence of typing constraints, existential variables can be
+duplicated in such a way that they possibly appear in different
+contexts than their defining context. Thus, any occurrence of a given
+existential variable comes with an instance of its original context. In the
+simple case, when an existential variable denotes the placeholder
+which generated it, or is used in the same context as the one in which
+it was generated, the context is not displayed and the existential
+variable is represented by ``?'' followed by an identifier.
+
+\begin{coq_example}
+Parameter identity : forall (X:Set), X -> X.
+Check identity _ _.
+Check identity _ (fun x => _).
+\end{coq_example}
+
+In the general case, when an existential variable ?{\ident}
+appears outside of its context of definition, its instance, written under
+the form \verb!@{id1:=term1; ...; idn:=termn}!, is appending to its
+name, indicating how the variables of its defining context are
+instantiated.  The variables of the context of the existential
+variables which are instantiated by themselves are not written, unless
+the flag {\tt Printing Existential Instances} is on (see
+Section~\ref{SetPrintingExistentialInstances}), and this is why an
+existential variable used in the same context as its context of
+definition is written with no instance.
+
+\begin{coq_example}
+Check (fun x y => _) 0 1.
+Set Printing Existential Instances.
+Check (fun x y => _) 0 1.
+\end{coq_example}
+
+\begin{coq_eval}
+Unset Printing Existential Instances.
+\end{coq_eval}
 
 \subsection{Explicit displaying of existential instances for pretty-printing
+\label{SetPrintingExistentialInstances}
 \comindex{Set Printing Existential Instances}
 \comindex{Unset Printing Existential Instances}}
 
@@ -1960,10 +1990,11 @@ The command:
 \begin{quote}
 {\tt Set Printing Existential Instances}
 \end{quote}
-activates the display of how the context of an existential variable is
-instantiated on each of its occurrences.
+activates the full display of how the context of an existential variable is
+instantiated at each of the occurrences of the existential variable.
 
-To deactivate the display of the instances of existential variables, use
+To deactivate the full display of the instances of existential
+variables, use
 \begin{quote}
 {\tt Unset Printing Existential Instances.}
 \end{quote}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index eabb37639..df707ce94 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -239,7 +239,7 @@ proof was edited.
 
 This command instantiates an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
-displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
+displayed by {\tt Show Existentials} (described in Section~\ref{Show}).
 
 This command is intended to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1b7adc251..35da17d54 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -260,6 +260,7 @@ Defined.
 \subsection{\tt apply \term}
 \tacindex{apply}
 \label{apply}
+\label{eapply}
 
 This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context.  The tactic {\tt apply} tries to
@@ -329,14 +330,13 @@ Section~\ref{pattern} to transform the goal so that it gets the form
    generated by {\tt apply} {\term$_i$}, starting from the application
    of {\term$_1$}.
 
-\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
+\item {\tt eapply \term}\tacindex{eapply}
 
   The tactic {\tt eapply} behaves like {\tt apply} but it does not fail
   when no instantiations are deducible for some variables in the
-  premises.  Rather, it turns these variables into so-called
-  existential variables which are variables still to instantiate. An
-  existential variable is identified by a name of the form {\tt ?$n$}
-  where $n$ is a number.  The instantiation is intended to be found
+  premises. Rather, it turns these variables into 
+  existential variables which are variables still to instantiate (see
+  Section~\ref{evars}). The instantiation is intended to be found
   later in the proof.
 
 \item {\tt simple apply {\term}} \tacindex{simple apply}
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index b6f63a3ba..a0949ca0c 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -8,6 +8,8 @@
 
 type mode = [ `FIND | `REPLACE ]
 
+let b2c = Ideutils.byte_offset_to_char_offset
+
 class finder name (view : GText.view) =
   
   let widget = Wg_Detachable.detachable
@@ -61,8 +63,10 @@ class finder name (view : GText.view) =
     method replace () =
       if self#may_replace () then
         let txt = self#get_selected_word () in
+        let () = view#buffer#begin_user_action () in
         let _ = view#buffer#delete_selection () in
         let _ = view#buffer#insert_interactive (self#replacement txt) in
+        let () = view#buffer#end_user_action () in
         self#find_forward ()
       else self#find_forward ()
 
@@ -85,8 +89,8 @@ class finder name (view : GText.view) =
       try
         let i = Str.search_backward regexp text (String.length text - 1) in
         let j = Str.match_end () in
-        Some(view#buffer#start_iter#forward_chars i,
-             view#buffer#start_iter#forward_chars j)
+        Some(view#buffer#start_iter#forward_chars (b2c text i),
+             view#buffer#start_iter#forward_chars (b2c text j))
       with Not_found -> None
     
     method private forward_search starti =
@@ -95,7 +99,7 @@ class finder name (view : GText.view) =
       try
         let i = Str.search_forward regexp text 0 in
         let j = Str.match_end () in
-        Some(starti#forward_chars i, starti#forward_chars j)
+        Some(starti#forward_chars (b2c text i), starti#forward_chars (b2c text j))
       with Not_found -> None
 
     method replace_all () =
@@ -115,7 +119,9 @@ class finder name (view : GText.view) =
           let () = view#buffer#delete_mark (`MARK stop_mark) in
           replace_at next
       in
-      replace_at view#buffer#start_iter
+      let () = view#buffer#begin_user_action () in
+      let () = replace_at view#buffer#start_iter in
+      view#buffer#end_user_action ()
 
     method private set_not_found () =
       find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"];
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index ce88ea6d2..85f18a093 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,10 +634,12 @@ and pp_module_type params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (mp, sign) ->
       push_visible mp params;
-      let try_pp_specif x l =
+      let try_pp_specif l x =
 	try pp_specif x :: l with Failure "empty phrase" -> l
       in
-      let l = List.fold_right try_pp_specif sign [] in
+      (* We cannot use fold_right here due to side effects in pp_specif *)
+      let l = List.fold_left try_pp_specif [] sign in
+      let l = List.rev l in
       pop_visible ();
       str "sig " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -710,10 +712,12 @@ and pp_module_expr params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEstruct (mp, sel) ->
       push_visible mp params;
-      let try_pp_structure_elem x l =
+      let try_pp_structure_elem l x =
 	try pp_structure_elem x :: l with Failure "empty phrase" -> l
       in
-      let l = List.fold_right try_pp_structure_elem sel [] in
+      (* We cannot use fold_right here due to side effects in pp_structure_elem *)
+      let l = List.fold_left try_pp_structure_elem [] sel in
+      let l = List.rev l in
       pop_visible ();
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 3403fb9c3..8a2d6e7bd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -446,6 +446,16 @@ let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ i
 
 let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
 
+(* Display a list of evars given by their name, with a prefix *)
+let pr_ne_evar_set hd tl sigma l =
+  if l != Evar.Set.empty then
+    let l = Evar.Set.fold (fun ev ->
+      Evar.Map.add ev (Evarutil.nf_evar_info sigma (Evd.find sigma ev)))
+      l Evar.Map.empty in
+    hd ++ pr_evars sigma l ++ tl
+  else
+    mt ()
+
 let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
diff --git a/printing/printer.mli b/printing/printer.mli
index 6b9c70815..42ed2b6d9 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -137,6 +137,8 @@ val pr_nth_open_subgoal    : int -> std_ppcmds
 val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
+val pr_ne_evar_set         : std_ppcmds -> std_ppcmds -> evar_map ->
+  Evar.Set.t -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1f1248d7..07969c7d7 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
diff --git a/test-suite/bugs/closed/3798.v b/test-suite/bugs/closed/3798.v
new file mode 100644
index 000000000..623822e99
--- /dev/null
+++ b/test-suite/bugs/closed/3798.v
@@ -0,0 +1,11 @@
+Require Setoid.
+
+Parameter f : nat -> nat.
+Axiom a : forall n, 0 < n -> f n = 0.
+Hint Rewrite a using ( simpl; admit ).
+
+Goal f 1 = 0.
+Proof.
+  rewrite_strat (topdown (hints core)).
+  reflexivity.
+Qed.
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e6b238286..fbc45b4ae 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -85,7 +85,7 @@ let _ =
     { optsync  = true;
       optdepr  = false;
       optname  = "automatic declaration of boolean equality";
-      optkey   = ["Equality";"Schemes"];
+      optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
 let _ = (* compatibility *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb12edfbc..bb2073001 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1516,12 +1516,8 @@ let vernac_check_may_eval redexp glopt rc =
         let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
 	msg_notice (print_judgment env sigma' j ++
-                    (if l != Evar.Set.empty then
-                        let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in
-                        (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l)
-                     else
-                        mt ()) ++
-                     Printer.pr_universe_ctx uctx)
+                    pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
+                    Printer.pr_universe_ctx uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in