21 files changed, 481 insertions, 169 deletions
diff --git a/CHANGES b/CHANGES
index 2cc91bbd6..a9fbfe29d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,9 +36,11 @@ Tactics
   introducing along pattern p changed to p%c1..%cn. The feature and
   syntax are in experimental stage.
 - "Proof using" does not clear unused section variables.
-- "refine" has been changed back to the 8.4 behavior of shelving subgoals
-  that occur in other subgoals. The "refine" tactic of 8.5beta2 has been
+- Tactic "refine" has been changed back to the 8.4 behavior of shelving subgoals
+  that occur in other subgoals. The "refine" tactic of 8.5beta3 has been
   renamed "simple refine"; it does not shelve any subgoal.
+- New tactical "unshelve tac" which grab existential variables put on
+  the tactic shelve by the execution of "tac".
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
@@ -516,11 +518,9 @@ Interfaces
   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.
-
 - Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks
   to the COQ_COLORS environment variable, and their current state can
   be displayed with the -list-tags command line option.
-
 - Third party user interfaces can install their main loop in $COQLIB/toploop
   and call coqtop with the -toploop flag to select it.
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7f9da4eab..bb627f590 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -163,14 +163,14 @@ Constrarg
 Constrexpr_ops
 Genintern
 Notation_ops
-Topconstr
 Notation
 Dumpglob
+Syntax_def
+Smartlocate
+Topconstr
 Reserve
 Impargs
-Syntax_def
 Implicit_quantifiers
-Smartlocate
 Constrintern
 Modintern
 Constrextern
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8bb1cc331..6f8584988 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -5,9 +5,9 @@
 
 There are three \Coq~commands: 
 \begin{itemize}
-\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
-\item {\tt coqc} : The \Coq\ compiler (batch compilation).
-\item {\tt coqchk} : The \Coq\ checker (validation of compiled libraries)
+\item {\tt coqtop}: the \Coq\ toplevel (interactive mode);
+\item {\tt coqc}: the \Coq\ compiler (batch compilation);
+\item {\tt coqchk}: the \Coq\ checker (validation of compiled libraries).
 \end{itemize}
 The options are (basically) the same for the first two commands, and
 roughly described below. You can also look at the \verb!man! pages of
@@ -39,11 +39,10 @@ The {\tt coqc} command takes a name {\em file} as argument.  Then it
 looks for a vernacular file named {\em file}{\tt .v}, and tries to
 compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 
-\Warning The name {\em file} must be a regular {\Coq} identifier, as
-defined in the Section~\ref{lexical}. It
-must only contain letters, digits or underscores
-(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
-\verb+/bar/foo/to-to.v+.
+\Warning The name {\em file} should be a regular {\Coq} identifier, as
+defined in Section~\ref{lexical}. It should contain only letters, digits
+or underscores (\_). For instance, \verb+/bar/foo/toto.v+ is valid, but
+\verb+/bar/foo/to-to.v+ is invalid.
 
 \section[Customization]{Customization at launch time}
 
@@ -64,7 +63,7 @@ directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
 
-\section{By environment variables\label{EnvVariables}
+\subsection{By environment variables\label{EnvVariables}
 \index{Environment variables}\label{envars}}
 
 Load path can be specified to the \Coq\ system by setting up
@@ -93,13 +92,13 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
 
 \begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ %
 
-Add physical path {\em directory} to the {\ocaml} loadpath.
+  Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
 
-\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+\item[{\tt -Q} {\em directory} {\dirpath}]\ %
 
   Add physical path \emph{directory} to the list of directories where
   {\Coq} looks for a file and bind it to the the logical directory
@@ -109,147 +108,184 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -R} {\em directory} {\dirpath}]\
+\item[{\tt -R} {\em directory} {\dirpath}]\ %
 
   Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
   subdirectory structure of \emph{directory} recursively visible so
   that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
-  
+
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -top} {\dirpath}, {\tt -notop}]\ 
+\item[{\tt -top} {\dirpath}]\ %
+
+  Set the toplevel module name to {\dirpath} instead of {\tt Top}. Not
+  valid for {\tt coqc} as the toplevel module name is inferred from the
+  name of the output file.
+
+\item[{\tt -notop}]\ %
+
+  Use the empty logical path for the toplevel module name instead of {\tt
+    Top}. Not valid for {\tt coqc} as the toplevel module name is
+  inferred from the name of the output file.
+
+\item[{\tt -exclude-dir} {\em directory}]\ %
 
-  This sets the toplevel module name to {\dirpath}/the empty logical path instead
-  of {\tt Top}. Not valid for {\tt coqc}.
+  Exclude any subdirectory named {\em directory} while
+  processing options such as {\tt -R} and {\tt -Q}. By default, only the
+  conventional version control management directories named {\tt CVS} and
+  {\tt \_darcs} are excluded.
 
-\item[{\tt -exclude-dir} {\em subdirectory}]\ 
+\item[{\tt -nois}]\ %
 
-  This tells to exclude any subdirectory named {\em subdirectory}
-  while processing option {\tt -R}. Without this option only the
-  conventional version control management subdirectories named {\tt
-  CVS} and {\tt \_darcs} are excluded.
+  Start from an empty state instead of loading the {\tt Init.Prelude}
+  module.
 
-\item[{\tt -nois}]\ 
+\item[{\tt -init-file} {\em file}]\ %
 
-  Cause \Coq~to begin with an empty state.
+  Load {\em file} as the resource file instead of loading the default
+  resource file from the standard configuration directories.
 
-\item[{\tt -init-file} {\em file}, {\tt -q}]\ 
+\item[{\tt -q}]\ %
 
-  Take {\em file} as the resource file. /
-  Cause \Coq~not to load the resource file.
+  Do not to load the default resource file.
 
-\item[{\tt -load-ml-source} {\em file}]\ 
+\item[{\tt -load-ml-source} {\em file}]\ %
 
   Load the {\ocaml} source file {\em file}.
 
-\item[{\tt -load-ml-object} {\em file}]\ 
+\item[{\tt -load-ml-object} {\em file}]\ %
 
   Load the {\ocaml} object file {\em file}.
 
-\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ 
+\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+
+\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em
+    file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+  Output its content on the standard input as it is executed.
+
+\item[{\tt -load-vernac-object} {\dirpath}]\ %
+
+  Load \Coq~compiled library {\dirpath}. This is equivalent to running
+  {\tt Require} {\dirpath}.
 
-  Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
-  standard input.
+\item[{\tt -require} {\dirpath}]\ %
 
-\item[{\tt -load-vernac-object} {\em path}]\ 
+  Load \Coq~compiled library {\dirpath} and import it. This is equivalent
+  to running {\tt Require Import} {\dirpath}.
 
-  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
+\item[{\tt -batch}]\ %
 
-\item[{\tt -require} {\em path}]\ 
+  Exit just after argument parsing. Available for {\tt coqtop} only.
 
-  Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
-    Require Import} {\em path}).
+\item[{\tt -compile} {\em file.v}]\ %
 
-\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
+  Compile file {\em file.v} into {\em file.vo}. This options imply {\tt
+    -batch} (exit just after argument parsing). It is available only
+  for {\tt coqtop}, as this behavior is the purpose of {\tt coqc}.
 
-  {\tt coqtop} options only used internally by {\tt coqc}.
+\item[{\tt -compile-verbose} {\em file.v}]\ %
 
-  This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
-  copy of the contents of the file on standard input.  This option implies options
-  {\tt -batch} (exit just after arguments parsing). It is only
-  available for {\tt coqtop}.
+  Same as {\tt -compile} but also output the content of {\em file.v} as
+  it is compiled.
 
-\item[{\tt -verbose}]\ 
+\item[{\tt -verbose}]\ %
 
-  This option is only for {\tt coqc}. It tells to compile the file with
-  a copy of its contents on standard input.
+  Output the content of the input file as it is compiled. This option is
+  available for {\tt coqc} only; it is the counterpart of {\tt
+    -compile-verbose}.
 
 %Mostly unused in the code
-%\item[{\tt -debug}]\ 
+%\item[{\tt -debug}]\ %
 %
 %  Switch on the debug flag.
 
-\item[{\tt -with-geoproof} (yes|no)]\ 
+\item[{\tt -with-geoproof} (yes|no)]\ %
 
-  Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
+  Enable or not special functions for Geoproof within {\CoqIDE} (default
+  is yes).
 
-\item[{\tt -color} (on|off|auto)]\
+\item[{\tt -color} (on|off|auto)]\ %
 
-  Activate or not the coloring of output of {\tt coqtop}. The default, auto,
-  means that {\tt coqtop} will dynamically decide whether to activate it
-  depending if the output channels of {\tt coqtop} can handle ANSI styles.
+  Enable or not the coloring of output of {\tt coqtop}. Default is auto,
+  meaning that {\tt coqtop} dynamically decides, depending on whether the
+  output channel supports ANSI escape sequences.
 
-\item[{\tt -beautify}]\ 
+\item[{\tt -beautify}]\ %
 
-  While compiling {\em file}, pretty prints each command just after having parsing
-  it in {\em file}{\tt .beautified} in order to get old-fashion
-  syntax/definitions/notations.
+  Pretty-print each command to {\em file.beautified} when compiling {\em
+    file.v}, in order to get old-fashioned syntax/definitions/notations.
 
-\item[{\tt -emacs}, {\tt -ide-slave}]\ 
+\item[{\tt -emacs}, {\tt -ide-slave}]\ %
 
-  Start a special main loop to communicate with ide.
+  Start a special toplevel to communicate with a specific IDE.
 
-\item[{\tt -impredicative-set}]\ 
+\item[{\tt -impredicative-set}]\ %
 
   Change the logical theory of {\Coq} by declaring the sort {\tt Set}
-  impredicative; warning: this is known to be inconsistent with
+  impredicative. Warning: this is known to be inconsistent with
   some standard axioms of classical mathematics such as the functional
-  axiom of choice or the principle of description
+  axiom of choice or the principle of description.
 
-\item[{\tt -type-in-type}]\
+\item[{\tt -type-in-type}]\ %
 
-  This collapses the universe hierarchy of {\Coq} making the logic inconsistent.
+  Collapse the universe hierarchy of {\Coq}. Warning: this makes the
+  logic inconsistent.
 
-\item[{\tt -compat} {\em version}] \mbox{}
+\item[{\tt -compat} {\em version}]\ %
 
-  Attempt to maintain some of the incompatible changes in their {\em version}
-  behavior.
+  Attempt to maintain some backward-compatibility with a previous version.
 
-\item[{\tt -dump-glob} {\em file}]\ 
+\item[{\tt -dump-glob} {\em file}]\ %
 
-  This dumps references for global names in file {\em file}
-  (to be used by coqdoc, see~\ref{coqdoc})
+  Dump references for global names in file {\em file} (to be used
+  by {\tt coqdoc}, see~\ref{coqdoc}). By default, if {\em file.v} is being
+  compiled, {\em file.glob} is used.
 
-\item[{\tt -no-hash-consing}] \mbox{}
+\item[{\tt -no-glob}]\ %
 
-\item[{\tt -image} {\em file}]\ 
+  Disable the dumping of references for global names.
 
-  This option sets the binary image to be used by {\tt coqc} to be {\em file}
+%\item[{\tt -no-hash-consing}]\ %
+
+\item[{\tt -image} {\em file}]\ %
+
+  Set the binary image to be used by {\tt coqc} to be {\em file}
   instead of the standard one. Not of general use.
 
-\item[{\tt -bindir} {\em directory}]\ 
+\item[{\tt -bindir} {\em directory}]\ %
+
+  Set the directory containing {\Coq} binaries to be used by {\tt coqc}.
+  It is equivalent to doing \texttt{export COQBIN=}{\em directory} before
+  launching {\tt coqc}.
+
+\item[{\tt -where}]\ %
+
+  Print the location of \Coq's standard library and exit.
 
-  Set for {\tt coqc} the directory containing \Coq\ binaries.
-  It is equivalent to do \texttt{export COQBIN=}{\em directory}
-  before launching {\tt coqc}.
+\item[{\tt -config}]\ %
 
-\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\ 
+  Print the locations of \Coq's binaries, dependencies, and libraries, then exit.
 
-  Print the \Coq's standard library location or \Coq's binaries, dependencies,
-  libraries locations or the list of command line arguments that {\tt coqtop} has
-  recognize as options and exit.
+\item[{\tt -filteropts}]\ %
 
-\item[{\tt -v}]\ 
+  Print the list of command line arguments that {\tt coqtop} has
+  recognized as options and exit.
 
-  Print the \Coq's version and exit.
+\item[{\tt -v}]\ %
 
-\item[{\tt -list-tags}]\
+  Print \Coq's version and exit.
 
-  Print the highlight tags known by \Coq as well as their currently associated
-  color.
+\item[{\tt -list-tags}]\ %
 
-\item[{\tt -h}, {\tt --help}]\ 
+  Print the highlight tags known by {\Coq} as well as their currently associated
+  color and exit.
+
+\item[{\tt -h}, {\tt --help}]\ %
 
   Print a short usage and exit.
 
@@ -293,18 +329,21 @@ Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
 same meaning as for {\tt coqtop}. Extra options are:
 \begin{description}
-\item[{\tt -norec} $module$]\ 
+\item[{\tt -norec} {\em module}]\ %
+
+  Check {\em module} but do not check its dependencies.
 
-  Check $module$ but do not force check of its dependencies.
-\item[{\tt -admit} $module$] \
+\item[{\tt -admit} {\em module}]\ %
 
-  Do not check $module$ and any of its dependencies, unless
+  Do not check {\em module} and any of its dependencies, unless
   explicitly required.
-\item[{\tt -o}]\ 
+
+\item[{\tt -o}]\ %
 
   At exit, print a summary about the context. List the names of all
   assumptions and variables (constants without body).
-\item[{\tt -silent}]\ 
+
+\item[{\tt -silent}]\ %
 
   Do not write progress information in standard output.
 \end{description}
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 7227f4b7b..4ebb484e7 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -17,10 +17,11 @@ The \Coq\ library is structured into two parts:
 
 In addition, user-provided libraries or developments are provided by
 \Coq\ users' community. These libraries and developments are available
-for download at \texttt{http://coq.inria.fr} (see
+for download at \url{http://coq.inria.fr} (see
 Section~\ref{Contributions}).
 
-The chapter briefly reviews the \Coq\ libraries.
+The chapter briefly reviews the \Coq\ libraries whose contents can
+also be browsed at \url{http://coq.inria.fr/stdlib}.
 
 \section[The basic library]{The basic library\label{Prelude}}
 
@@ -799,7 +800,9 @@ At the end, it defines data-types at the {\Type} level.
 \subsection{Tactics}
 
 A few tactics defined at the user level are provided in the initial
-state\footnote{This is in module {\tt Tactics.v}}.
+state\footnote{This is in module {\tt Tactics.v}}. They are listed at
+\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt
+  Tactics}).
 
 \section{The standard library}
 
@@ -842,7 +845,7 @@ Chapter~\ref{Other-commands}).
 The different modules of the \Coq\ standard library are described in the
 additional document \verb!Library.dvi!. They are also accessible on the WWW
 through the \Coq\ homepage
-\footnote{\texttt{http://coq.inria.fr}}.
+\footnote{\url{http://coq.inria.fr}}.
 
 \subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
@@ -1035,7 +1038,7 @@ intros; split_Rmult.
 
 \end{itemize}
 
-All this tactics has been written with the tactic language Ltac
+These tactics has been written with the tactic language Ltac
 described in Chapter~\ref{TacticLanguage}.
 
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f268d8276..815594d8e 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -864,16 +864,17 @@ introduction pattern~$p$:
   expects the product to be over an inductive type
   whose number of constructors is $n$ (or more generally over a type
   of conclusion an inductive type built from $n$ constructors,
-  e.g. {\tt C -> A\textbackslash/B if $n=2$}): it destructs the introduced
+  e.g. {\tt C -> A\textbackslash/B} with $n=2$ since {\tt
+    A\textbackslash/B} has 2 constructors): it destructs the introduced
   hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and
   applies on each generated subgoal the corresponding tactic;
   \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
-  pattern is part of a sequence of patterns and is not the last
-  pattern of the sequence, then {\Coq} completes the pattern so that all
-  the argument of the constructors of the inductive type are
-  introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H}
-  applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as
-  the list of patterns {\tt [$\,$|$\,$?$\,$] H});
+  pattern is part of a sequence of patterns, then {\Coq} completes the
+  pattern so that all the arguments of the constructors of the
+  inductive type are introduced (for instance, the list of patterns
+  {\tt [$\;$|$\;$] H} applied on goal {\tt forall x:nat, x=0 -> 0=x}
+  behaves the same as the list of patterns {\tt [$\,$|$\,$?$\,$] H},
+  up to one exception explained in the Remark below);
 \item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
   $p_n$)} expects the goal to be a product over an inductive type $I$ with a
   single constructor that itself has at least $n$ arguments: it
@@ -887,10 +888,10 @@ introduction pattern~$p$:
   {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
   hypothesis to be a sequence of right-associative binary inductive
   constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
-  hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+  hypothesis with type {\tt A\verb|/\|(exists x, B\verb|/\|C\verb|/\|D)} can be
   introduced via pattern {\tt (a \& x \& b \& c \& d)};
 \item if the product is over an equality type, then a pattern of the
-  form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
+  form {\tt [= $p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
   (see Section~\ref{injection}) or {\tt discriminate} (see
   Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt
     injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are
@@ -950,6 +951,7 @@ Abort.
 
 \Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
 \texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
+\label{bracketing-last}
 \begin{itemize}
 \item A wildcard pattern never succeeds when applied isolated on a
   dependent product, while it succeeds as part of a list of
@@ -971,6 +973,13 @@ Show 2.
 
 \end{itemize}
 
+This later behavior can be avoided by setting the following option:
+
+\begin{quote}
+\optindex{Bracketing Last Introduction Pattern}
+{\tt Set Bracketing Last Introduction Pattern}
+\end{quote}
+
 \subsection{\tt clear \ident}
 \tacindex{clear}
 \label{clear}
@@ -1459,6 +1468,24 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
+\subsection{\tt admit}
+\tacindex{admit}
+\tacindex{give\_up}
+\label{admit}
+
+The {\tt admit} tactic allows temporarily skipping a subgoal so as to
+progress further in the rest of the proof.  A proof containing
+admitted goals cannot be closed with {\tt Qed} but only with
+{\tt Admitted}.
+
+\begin{Variants}
+
+  \item {\tt give\_up}
+
+    Synonym of {\tt admit}.
+
+\end{Variants}
+
 \subsection{\tt absurd \term}
 \tacindex{absurd}
 \label{absurd}
@@ -4113,6 +4140,7 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by
 
 \subsection{\tt tauto}
 \tacindex{tauto}
+\tacindex{dtauto}
 \label{tauto}
 
 This tactic implements a decision procedure for intuitionistic propositional
@@ -4161,8 +4189,21 @@ Abort.
 because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
 instantiation of \verb=x= is necessary.
 
+\begin{Variants}
+
+\item {\tt dtauto}
+
+  While {\tt tauto} recognizes inductively defined connectives
+  isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+    or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+    True}, {\tt dtauto} recognizes also all inductive types with
+  one constructors and no indices, i.e. record-style connectives.
+
+\end{Variants}
+
 \subsection{\tt intuition \tac}
 \tacindex{intuition}
+\tacindex{dintuition}
 \label{intuition}
 
 The tactic \texttt{intuition} takes advantage of the search-tree built
@@ -4195,8 +4236,49 @@ incompatibilities.
 \item {\tt intuition}
 
   Is equivalent to {\tt intuition auto with *}.
+
+\item {\tt dintuition}
+
+  While {\tt intuition} recognizes inductively defined connectives
+  isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+    or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+    True}, {\tt dintuition} recognizes also all inductive types with
+  one constructors and no indices, i.e. record-style connectives.
+
 \end{Variants}
 
+\optindex{Intuition Negation Unfolding}
+\optindex{Intuition Iff Unfolding}
+
+Some aspects of the tactic {\tt intuition} can be
+controlled using options. To avoid that inner negations which do not
+need to be unfolded are unfolded, use:
+
+\begin{quote}
+{\tt Unset Intuition Negation Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Negation Unfolding}
+\end{quote}
+
+To avoid that inner occurrence of {\tt iff} which do not need to be
+unfolded are unfolded (this is the default), use:
+
+\begin{quote}
+{\tt Unset Intuition Iff Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Iff Unfolding}
+\end{quote}
+
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
diff --git a/interp/interp.mllib b/interp/interp.mllib
index c9a031526..96b52959a 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,12 +3,12 @@ Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
-Topconstr
 Ppextend
 Notation
 Dumpglob
 Syntax_def
 Smartlocate
+Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 837630183..db38a85d4 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -38,27 +38,11 @@ let error_invalid_pattern_notation loc =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-let ids_of_cases_indtype =
-  let rec vars_of ids = function
-    (* We deal only with the regular cases *)
-    | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) ->
-      List.fold_left vars_of (List.fold_left vars_of [] l2) l1
-    (* assume the ntn is applicative and does not instantiate the head !! *)
-    | CPatDelimiters(_,_,c) -> vars_of ids c
-    | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids
-    | _ -> ids in
-  vars_of []
-
-let ids_of_cases_tomatch tms =
-  List.fold_right
-    (fun (_,ona,indnal) l ->
-      Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
-      indnal (Option.fold_right (Loc.down_located name_cons) ona l))
-    tms []
-
 let is_constructor id =
-  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
-  with Not_found -> true
+  try Globnames.isConstructRef
+        (Smartlocate.global_of_extended_global
+           (Nametab.locate_extended (qualid_of_ident id)))
+  with Not_found -> false
 
 let rec cases_pattern_fold_names f a = function
   | CPatRecord (_, l) ->
@@ -82,6 +66,17 @@ let ids_of_pattern_list =
       (List.fold_left (cases_pattern_fold_names Id.Set.add)))
     Id.Set.empty
 
+let ids_of_cases_indtype p =
+  Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p)
+
+let ids_of_cases_tomatch tms =
+  List.fold_right
+    (fun (_, ona, indnal) l ->
+      Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+      indnal
+        (Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
+    tms Id.Set.empty
+
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
@@ -119,7 +114,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
-      let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
+      let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
@@ -220,10 +215,11 @@ let map_constr_expr_with_binders g f e = function
   | CPrim _ | CRef _ as x -> x
   | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
-      (* TODO: apply g on the binding variables in pat... *)
-      let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
+      let bl = List.map (fun (loc,patl,rhs) ->
+        let ids = ids_of_pattern_list patl in
+        (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
       let ids = ids_of_cases_tomatch a in
-      let po = Option.map (f (List.fold_right g ids e)) rtnpo in
+      let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 331598d85..b5cfeeba7 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -74,7 +74,17 @@ let call_compiler ml_filename =
     ::include_dirs
     @ ["-impl"; ml_filename] in
   if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
-  try CUnix.sys_command (ocamlfind ()) args = Unix.WEXITED 0, link_filename
+  try
+    let res = CUnix.sys_command (ocamlfind ()) args in
+    let res = match res with
+      | Unix.WEXITED 0 -> true
+      | Unix.WEXITED n ->
+         Pp.(msg_warning (str "command exited with status " ++ int n)); false
+      | Unix.WSIGNALED n ->
+         Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+      | Unix.WSTOPPED n ->
+         Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+    res, link_filename
   with Unix.Unix_error (e,_,_) ->
     Pp.(msg_warning (str (Unix.error_message e)));
     false, link_filename
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 659990806..fc7c074cc 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -110,7 +110,6 @@ val replace_vars : (Id.t * constr) list -> constr -> constr
    then Γ\\{id₁,...,id{_n}\},x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ [substn_vars
    (|Γ'|+1) [id₁;...;idn] t] : [substn_vars (|Γ'|+1) [id₁;...;idn]
    T]. *)
-
 val substn_vars : int -> Id.t list -> constr -> constr
 
 (** [subst_vars [id1;...;idn] t] is a short-hand for [substn_vars
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 84beaa9e3..4f9fbddda 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -178,22 +178,26 @@ type inference_flags = {
   expand_evars : bool
 }
 
+let frozen_holes (sigma, sigma') =
+  let fold evk _ accu = Evar.Set.add evk accu in
+  Evd.fold_undefined fold sigma Evar.Set.empty
+
 let pending_holes (sigma, sigma') =
   let fold evk _ accu =
     if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
   in
   Evd.fold_undefined fold sigma' Evar.Set.empty
 
-let apply_typeclasses env evdref pending fail_evar =
-  let filter_pending evk = Evar.Set.mem evk pending in
+let apply_typeclasses env evdref frozen fail_evar =
+  let filter_frozen evk = Evar.Set.mem evk frozen in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
-	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && filter_pending evk)
-              else (fun evk evi -> Typeclasses.no_goals evk evi && filter_pending evk))
+	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
+              else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
      ~split:true ~fail:fail_evar env !evdref;
   if Flags.is_program_mode () then (* Try optionally solving the obligations *)
     evdref := Typeclasses.resolve_typeclasses
-      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && filter_pending evk) ~split:true ~fail:false env !evdref
+      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
 
 let apply_inference_hook hook evdref pending =
   evdref := Evar.Set.fold (fun evk sigma ->
@@ -214,9 +218,9 @@ let apply_heuristics env evdref fail_evar =
   with e when Errors.noncritical e ->
     let e = Errors.push e in if fail_evar then iraise e
 
-let check_typeclasses_instances_are_solved env current_sigma pending =
+let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env (ref current_sigma) pending true
+  apply_typeclasses env (ref current_sigma) frozen true
 
 let check_extra_evars_are_solved env current_sigma pending =
   Evar.Set.iter
@@ -228,26 +232,28 @@ let check_extra_evars_are_solved env current_sigma pending =
 	| _ ->
 	    error_unsolvable_implicit loc env current_sigma evk None) pending
 
-let check_evars_are_solved env current_sigma pending =
-  check_typeclasses_instances_are_solved env current_sigma pending;
+let check_evars_are_solved env current_sigma frozen pending =
+  check_typeclasses_instances_are_solved env current_sigma frozen;
   check_problems_are_solved env current_sigma;
   check_extra_evars_are_solved env current_sigma pending
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars flags env current_sigma pending =
+  let frozen = frozen_holes pending in
   let pending = pending_holes pending in
   let evdref = ref current_sigma in
-  if flags.use_typeclasses then apply_typeclasses env evdref pending false;
+  if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
     apply_inference_hook (Option.get flags.use_hook env) evdref pending;
   if flags.use_unif_heuristics then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env !evdref pending;
+  if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
   !evdref
 
 let check_evars_are_solved env current_sigma pending =
+  let frozen = frozen_holes pending in
   let pending = pending_holes pending in
-  check_evars_are_solved env current_sigma pending
+  check_evars_are_solved env current_sigma frozen pending
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
   let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b42a70b34..0a75510c3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -38,6 +38,8 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> keyed_unification:=a);
 }
 
+let is_keyed_unification () = !keyed_unification
+
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
@@ -1671,8 +1673,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
     let cl = strip_outer_cast cl in
     (try
        if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then
-	 (try w_typed_unify env evd CONV flags op cl,cl
-	  with ex when Pretype_errors.unsatisfiable_exception ex ->
+       (try
+         if !keyed_unification then
+           let f1, l1 = decompose_app_vect op in
+	   let f2, l2 = decompose_app_vect cl in
+	   w_typed_unify_array env evd flags f1 l1 f2 l2,cl
+	 else w_typed_unify env evd CONV flags op cl,cl
+       with ex when Pretype_errors.unsatisfiable_exception ex ->
 	    bestexn := Some ex; error "Unsat")
        else error "Bound 1"
      with ex when precatchable_exception ex ->
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 14bcb4a06..9ce24c70e 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -42,6 +42,8 @@ val default_no_delta_unify_flags : unit -> unify_flags
 val elim_flags : unit -> unify_flags
 val elim_no_delta_flags : unit -> unify_flags
 
+val is_keyed_unification : unit -> bool
+
 (** The "unique" unification fonction *)
 val w_unify :
   env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ac41c9464..602917050 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -206,9 +206,47 @@ let rewrite_conv_closed_unif_flags = {
   resolve_evars = false
 }
 
+let rewrite_keyed_core_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+    (* We have this flag for historical reasons, it has e.g. the consequence *)
+    (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
+
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
+    (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
+    (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
+
+  modulo_delta = full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = true;
+  use_pattern_unification = true;
+    (* To rewrite "?n x y" in "y+x=0" when ?n is *)
+    (* a preexisting evar of the goal*)
+
+  use_meta_bound_pattern_unification = true;
+
+  frozen_evars = Evar.Set.empty;
+    (* This is set dynamically *)
+
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = true;
+  (* Different from conv_closed *)
+  modulo_eta = true;
+}
+
+let rewrite_keyed_unif_flags = {
+  core_unify_flags = rewrite_keyed_core_unif_flags;
+  merge_unify_flags = rewrite_keyed_core_unif_flags;
+  subterm_unify_flags = rewrite_keyed_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
+}
+
 let rewrite_elim with_evars frzevars cls c e =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_conv_closed_unif_flags c in
+  let flags = if Unification.is_keyed_unification ()
+	      then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
+  let flags = make_flags frzevars (Tacmach.New.project gl) flags c in
   general_elim_clause with_evars flags cls c e
   end }
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index eddefb279..1b5525e67 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1525,12 +1525,13 @@ let assert_replacing id newt tac =
 let newfail n s = 
   Proofview.tclZERO (Refiner.FailError (n, lazy s))
 
-let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
+let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
-    | Some None -> Proofview.tclUNIT ()
+    | Some None -> if progress then newfail 0 (str"Failed to progress")
+		   else Proofview.tclUNIT ()
     | Some (Some res) ->
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1597,21 +1598,25 @@ let tactic_init_setoid () =
   try init_setoid (); tclIDTAC
   with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
 
-(** Setoid rewriting when called with "rewrite_strat" *)
-let cl_rewrite_clause_strat strat clause =
+let cl_rewrite_clause_strat progress strat clause =
   tclTHEN (tactic_init_setoid ())
-  (fun gl -> 
-     try Proofview.V82.of_tactic (cl_rewrite_clause_newtac strat clause) gl
-     with RewriteFailure e ->
-       errorlabstrm "" (str"setoid rewrite failed: " ++ e)
-     | Refiner.FailError (n, pp) -> 
-       tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)
+  ((if progress then tclWEAK_PROGRESS else fun x -> x)
+   (fun gl -> 
+    try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl
+    with RewriteFailure e ->
+	 errorlabstrm "" (str"setoid rewrite failed: " ++ e)
+       | Refiner.FailError (n, pp) -> 
+	  tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl))
 
 (** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause gl =
   let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
-    cl_rewrite_clause_strat strat clause gl
+    cl_rewrite_clause_strat true strat clause gl
 
+(** Setoid rewriting when called with "rewrite_strat" *)
+let cl_rewrite_clause_strat strat clause =
+  cl_rewrite_clause_strat false strat clause
+  
 let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
   let c sigma =
     let (sigma, c) = Pretyping.understand_tcc env sigma c in
@@ -2017,7 +2022,8 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
       tclWEAK_PROGRESS 
 	(tclTHEN
            (Refiner.tclEVARS evd)
-	   (Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~abs:(Some abs) ~origsigma strat cl))) gl
+	   (Proofview.V82.of_tactic
+	    (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) gl
     with RewriteFailure e ->
       tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl
 
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/closed/3848.v
index a03e8ffda..c0ef02f1e 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/closed/3848.v
@@ -19,4 +19,4 @@ Proof.
   refine (functor_forall
             (f^-1)
             (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
-Fail Defined. (* Error: Attempt to save an incomplete proof *)
+Defined. (* was: Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v
new file mode 100644
index 000000000..3cdc4ada0
--- /dev/null
+++ b/test-suite/bugs/closed/4256.v
@@ -0,0 +1,43 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Global Set Universe Polymorphism.
+Monomorphic Universe i.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+Notation "-1" := (trunc_S minus_two) (at level 0).
+
+Class IsPointed (A : Type) := point : A.
+Arguments point A {_}.
+
+Record pType :=
+  { pointed_type : Type ;
+    ispointed_type : IsPointed pointed_type }.
+Coercion pointed_type : pType >-> Sortclass.
+Existing Instance ispointed_type.
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+
+
+Record ooGroup :=
+  { classifying_space : pType@{i} }.
+
+Definition group_loops (X : pType)
+: ooGroup.
+Proof.
+  (** This works: *)
+  pose (x0 := point X).
+  pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)).
+  clear H x0.
+  (** But this doesn't: *)
+  pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v
new file mode 100644
index 000000000..6f8631d45
--- /dev/null
+++ b/test-suite/bugs/closed/4467.v
@@ -0,0 +1,15 @@
+(* Fixing missing test for variable shadowing *)
+
+Definition test (x y:bool*bool) :=
+  match x with
+  | (e as e1, (true) as e2)
+  | ((true) as e1, e as e2) =>
+    let '(e, b) := y in
+    e
+  | _ => true
+  end.
+
+Goal test (true,false) (true,true) = true.
+(* used to evaluate to "false = true" in 8.4 *)
+reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v
new file mode 100644
index 000000000..08a86330f
--- /dev/null
+++ b/test-suite/bugs/closed/4480.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Definition proj (P Q : Prop) := P.
+
+Lemma foo (P : Prop) : proj P P = P.
+Admitted.
+Lemma trueI : True <-> True.
+Admitted.
+Goal True.
+  Fail setoid_rewrite foo.
+  Fail setoid_rewrite trueI.
+  
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v
new file mode 100644
index 000000000..f988539d6
--- /dev/null
+++ b/test-suite/bugs/closed/4484.v
@@ -0,0 +1,10 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Class A := {}.
+Axiom foo : forall {ac : A}, bool.
+Lemma bar (ac : A) : True.
+Check (match foo as k return foo = k -> True with
+       | true => _
+       | false => _
+       end eq_refl).
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e42663505..49c465b6c 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1861,3 +1861,10 @@ Type (fun n => match n with
 
 Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
   match p with eq_refl => u end.
+
+(* Check in-pattern clauses with constant constructors, which were
+   previously interpreted as variables (before 8.5) *)
+
+Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
+
+Check match niln in listn O return O=O with niln => eq_refl end.
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index bbe9d4bff..5b0502cf1 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -22,3 +22,40 @@ Qed.
 
 Print Equivalent Keys.
 End foo.
+
+Require Import Arith List Omega.
+
+Definition G {A} (f : A -> A -> A) (x : A) := f x x.
+
+Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l.
+Proof. unfold G; rewrite app_nil_r; reflexivity. Qed.
+
+(* Bundled version of a magma *)
+Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }.
+Arguments op {_} _ _.
+
+(* Instance for lists *)
+Canonical Structure list_magma A := Magma (list A) (@app A).
+
+(* Basically like list_foo, but now uses the op projection instead of app for
+the argument of G *)
+Lemma test1 A (l : list A) : G op (l ++ nil) = G op l.
+
+(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *)
+rewrite -> list_foo.
+reflexivity.
+Qed.
+
+(* Basically like list_foo, but now uses the op projection for everything *)
+Lemma test2 A (l : list A) : G op (op l nil) = G op l.
+Proof.
+rewrite ->list_foo.
+reflexivity.
+Qed.
+
+ Require Import Bool.
+   Set Keyed Unification.
+
+   Lemma test b : b && true = b.
+    Fail rewrite andb_true_l.
+   Admitted.
+\ No newline at end of file