From 905e3dd364e8be20771c39393e7e114f2e4b8cd8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 6 Jan 2016 16:26:04 +0100
Subject: Fix description of command-line options in the manual.

---
 doc/refman/RefMan-com.tex | 225 +++++++++++++++++++++++++++-------------------
 1 file changed, 132 insertions(+), 93 deletions(-)

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8bb1cc331b..6f85849888 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}
-- 
cgit v1.2.3


From e309d8119cd82bdf1216751fb076d438782fb60f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 7 Jan 2016 17:20:51 +0100
Subject: Fix bug #4480: progress was not checked for setoid_rewrite.

Also ensure we stay compatible with 8.4: progress could now be made
simply because of beta redexes in the goal.
---
 tactics/rewrite.ml            | 15 ++++++++-------
 test-suite/bugs/closed/4480.v | 12 ++++++++++++
 2 files changed, 20 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/bugs/closed/4480.v

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a230ea251a..6d61879e89 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1526,7 +1526,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
-    | Some None -> Proofview.tclUNIT ()
+    | Some None -> newfail 0 (str"Failed to progress")
     | Some (Some res) ->
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1596,12 +1596,13 @@ let tactic_init_setoid () =
 (** Setoid rewriting when called with "rewrite_strat" *)
 let cl_rewrite_clause_strat 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)
+  (tclWEAK_PROGRESS
+   (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))
 
 (** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause gl =
diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v
new file mode 100644
index 0000000000..08a86330f2
--- /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
-- 
cgit v1.2.3


From 29d2dcb5474e4eed7e0f0d02d1e388bff53ec82d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 7 Jan 2016 17:21:54 +0100
Subject: Fix a misleading comment for substn_vars

---
 kernel/vars.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/vars.mli b/kernel/vars.mli
index c0fbeeb6e6..9f034b288a 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -65,7 +65,7 @@ val subst_var : Id.t -> constr -> constr
    if two names are identical, the one of least indice is kept *)
 val subst_vars : Id.t list -> constr -> constr
 
-(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+(** [substn_vars n [id1;...;idk] t] substitute [VAR idj] by [Rel j+n-1] in [t]
    if two names are identical, the one of least indice is kept *)
 val substn_vars : int -> Id.t list -> constr -> constr
 
-- 
cgit v1.2.3


From 8b0fbcc6568308794ef198f8e96093b00ba90ca4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 8 Jan 2016 10:46:26 +0100
Subject: Be more verbose about failure to compile libraries to native code.

On a machine with only 1GB of memory (e.g. in a VM), the compiler might be
abruptly killed by a segfault. We were not getting any feedback in that
case, making it harder to debug.
---
 kernel/nativelib.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index b2142b43c7..81470f9015 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -77,7 +77,17 @@ let call_compiler ml_filename =
     ::include_dirs
     @ ["-impl"; ml_filename] in
   if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args)));
-  try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename
+  try
+    let res = CUnix.sys_command compiler_name 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
-- 
cgit v1.2.3


From 35ffd67ae0ad50b7fa28669f78d4893b0f20f3ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 11 Jan 2016 10:18:52 +0100
Subject: Fix bug #3338 again, no progress is necessary for the success of
 rewrite_strat.

---
 tactics/rewrite.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6d61879e89..ec58ef25b1 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1521,12 +1521,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 -> newfail 0 (str"Failed to progress")
+    | 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
@@ -1593,12 +1594,11 @@ 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 ())
-  (tclWEAK_PROGRESS
+  ((if progress then tclWEAK_PROGRESS else fun x -> x)
    (fun gl -> 
-    try Proofview.V82.of_tactic (cl_rewrite_clause_newtac strat clause) 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) -> 
@@ -1607,8 +1607,12 @@ let cl_rewrite_clause_strat strat clause =
 (** 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
@@ -2014,7 +2018,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
 
-- 
cgit v1.2.3


From 4dbf44a47949adce5e538a7aacc670ec64c28d3f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 12 Jan 2016 10:39:49 +0100
Subject: restore documentation of admit

---
 doc/refman/RefMan-tac.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d90a027295..11d62b60a3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1468,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}
-- 
cgit v1.2.3


From 682ddc2d278b345c4c72da6c8a8d17cc82a076ec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 10:46:43 +0100
Subject: Documenting option 'Set Bracketing Last Introduction Pattern'.

---
 doc/refman/RefMan-tac.tex | 27 ++++++++++++++++++---------
 1 file changed, 18 insertions(+), 9 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 11d62b60a3..ce934871f3 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}
-- 
cgit v1.2.3


From f5de32ad1600cd18a6f1f286729c979e868ad088 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 11:32:54 +0100
Subject: Documenting options "Intuition Negation Unfolding", "Intuition Iff
 Unfolding".

---
 doc/refman/RefMan-tac.tex | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ce934871f3..b07cfb7d59 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4233,6 +4233,38 @@ incompatibilities.
   Is equivalent to {\tt intuition auto with *}.
 \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}
 
-- 
cgit v1.2.3


From e21e8c2804d047d4b80613e31bec0bc7320b7e8b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 11:48:45 +0100
Subject: Documenting dtauto and dintuition.

---
 doc/refman/RefMan-tac.tex | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b07cfb7d59..b3a730e675 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4149,6 +4149,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
@@ -4197,8 +4198,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
@@ -4231,6 +4245,15 @@ 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}
-- 
cgit v1.2.3


From 94b3068c688b289ec26005d13251fc1c3dae6998 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 12:14:41 +0100
Subject: Referring to coq.inria.fr/stdlib for more on libraries and ltac-level
 tactics.

---
 doc/refman/RefMan-lib.tex | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 7227f4b7b6..4ebb484e7c 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}
-- 
cgit v1.2.3


From 4841b790bbe517deefac11e8df1a7a1494d56bec Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 12 Jan 2016 17:02:09 +0100
Subject: Fix essential bug in new Keyed Unification mode reported by R.
 Krebbers.

[rewrite] was calling find_suterm using the wrong unification flags, not
allowing full delta in unification of terms with the right keys as desired.
---
 pretyping/unification.ml  |  2 ++
 pretyping/unification.mli |  2 ++
 tactics/equality.ml       | 40 +++++++++++++++++++++++++++++++++++++++-
 3 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9758aa43c4..510d5761b7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -37,6 +37,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;
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 119b1a7590..9246c10f90 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 fe0ca61c66..ccb0425f4a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -205,9 +205,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 begin fun gl ->
-  let flags = make_flags frzevars (Proofview.Goal.sigma 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 (Proofview.Goal.sigma gl) flags c in
   general_elim_clause with_evars flags cls c e
   end
 
-- 
cgit v1.2.3


From eb40037b4c341746933c713e8950f3a60d550f4a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 12 Jan 2016 17:32:04 +0100
Subject: Extend Keyed Unification tests with the one from R. Krebbers.

---
 test-suite/success/keyedrewrite.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index bbe9d4bfff..d1a93581ca 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -22,3 +22,34 @@ 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.
+
-- 
cgit v1.2.3


From fc642ca962dd5228a5a714b8e41506dcbc3b6520 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 12 Jan 2016 19:27:02 +0100
Subject: Extend last commit: keyed unification uses full conversions on the
 applied constant and arguments _separately_.

---
 pretyping/unification.ml          | 9 +++++++--
 test-suite/success/keyedrewrite.v | 6 ++++++
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 510d5761b7..48638474a8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1649,8 +1649,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/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index d1a93581ca..5b0502cf1a 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -53,3 +53,9 @@ 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
-- 
cgit v1.2.3


From 74d89e0be05e5cb4c9faf154478bc0c907bec2bb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Dec 2015 20:14:07 +0100
Subject: Reporting about the new tactical unshelve.

---
 CHANGES | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHANGES b/CHANGES
index b30bcc662d..531d5049fd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,9 +22,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
 ===================================
@@ -495,11 +497,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.
 
-- 
cgit v1.2.3


From be4bfc78c493464cb0af40d7fae08ba86295a6f9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 20:49:34 +0100
Subject: Fixing #4256 and #4484 (changes in evar-evar resolution made that new
 evars were created making in turn that evars formerly recognized as pending
 were not anymore in the list of pending evars). This also fixes the reopening
 of #3848.

See comments on #4484 for details.
---
 pretyping/pretyping.ml        | 30 ++++++++++++++++++------------
 test-suite/bugs/closed/3848.v | 22 ++++++++++++++++++++++
 test-suite/bugs/closed/4256.v | 43 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/4484.v | 10 ++++++++++
 test-suite/bugs/opened/3848.v | 22 ----------------------
 5 files changed, 93 insertions(+), 34 deletions(-)
 create mode 100644 test-suite/bugs/closed/3848.v
 create mode 100644 test-suite/bugs/closed/4256.v
 create mode 100644 test-suite/bugs/closed/4484.v
 delete mode 100644 test-suite/bugs/opened/3848.v

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index faba5c7563..521fa2247b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -183,22 +183,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 ->
@@ -219,9 +223,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
@@ -233,26 +237,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/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v
new file mode 100644
index 0000000000..a03e8ffdab
--- /dev/null
+++ b/test-suite/bugs/closed/3848.v
@@ -0,0 +1,22 @@
+Require Import TestSuite.admit.
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Generalizable Variables A B f g e n.
+Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
+           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
+: (forall a:A, P a) -> (forall b:B, Q b).
+  admit.
+Defined.
+
+Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
+      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
+: (forall b : B, Q b) -> forall a : A, P a.
+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 *)
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v
new file mode 100644
index 0000000000..3cdc4ada02
--- /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/4484.v b/test-suite/bugs/closed/4484.v
new file mode 100644
index 0000000000..f988539d62
--- /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/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
deleted file mode 100644
index a03e8ffdab..0000000000
--- a/test-suite/bugs/opened/3848.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Require Import TestSuite.admit.
-Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
-Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
-Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
-Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
-Arguments eisretr {A B} f {_} _.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
-Generalizable Variables A B f g e n.
-Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
-           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
-: (forall a:A, P a) -> (forall b:B, Q b).
-  admit.
-Defined.
-
-Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
-      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
-: (forall b : B, Q b) -> forall a : A, P a.
-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 *)
-- 
cgit v1.2.3


From 9f8ae1aa2678944888d80ce0867bfb2bba0c8c71 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 22:12:40 +0100
Subject: Fixing #4467 (missing shadowing of variables in cases pattern).

This fixes a TODO in map_constr_expr_with_binders, a bug in
is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
---
 interp/topconstr.ml           | 40 +++++++++++++++++-----------------------
 test-suite/bugs/closed/4467.v | 15 +++++++++++++++
 2 files changed, 32 insertions(+), 23 deletions(-)
 create mode 100644 test-suite/bugs/closed/4467.v

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1231f11555..560cd0277b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -38,27 +38,9 @@ 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
+  with Not_found -> false
 
 let rec cases_pattern_fold_names f a = function
   | CPatRecord (_, l) ->
@@ -82,6 +64,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 +112,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 fst al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
@@ -220,10 +213,11 @@ let map_constr_expr_with_binders g f e = function
   | CPrim _ | CRef _ as x -> x
   | CRecord (loc,p,l) -> CRecord (loc,p,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) -> (f e tm,x)) 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/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v
new file mode 100644
index 0000000000..6f8631d458
--- /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.
-- 
cgit v1.2.3


From 2d568a895d5c8a246f497c94c79811d3aad4269f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Jan 2016 00:20:46 +0100
Subject: Fixing #4467 (continued).

Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
---
 dev/printers.mllib         | 6 +++---
 interp/interp.mllib        | 2 +-
 interp/topconstr.ml        | 4 +++-
 test-suite/success/Cases.v | 7 +++++++
 4 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/dev/printers.mllib b/dev/printers.mllib
index eeca6809ae..ab7e9fc346 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -160,14 +160,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/interp/interp.mllib b/interp/interp.mllib
index c9a0315267..96b52959a0 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 560cd0277b..2cb2449b7d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -39,7 +39,9 @@ let error_invalid_pattern_notation loc =
 (* Functions on constr_expr *)
 
 let is_constructor id =
-  try ignore (Nametab.locate_extended (qualid_of_ident id)); 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
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e42663505d..49c465b6c6 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.
-- 
cgit v1.2.3


From 245affffb174fb26fc9a847abe44e01b107980a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Jan 2016 00:48:37 +0100
Subject: Fixing success of test for #3848 after move to directory "closed".

---
 test-suite/bugs/closed/3848.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v
index a03e8ffdab..c0ef02f1e8 100644
--- a/test-suite/bugs/closed/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 *)
-- 
cgit v1.2.3