Merge branch 'v8.5'

14 files changed, 370 insertions, 99 deletions

diff --git a/CHANGES b/CHANGES
index 3f7cc7c98..921688664 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,80 @@ Notations
 
 - "Bind Scope" can once again bind "Funclass" and "Sortclass".
 
+Changes from V8.5pl1 to V8.5pl2
+===============================
+
+Bugfixes
+
+- #4677: fix alpha-conversion in notations needing eta-expansion
+
+Changes from V8.5 to V8.5pl1
+============================
+
+Critical bugfix
+- The subterm relation for the guard condition was incorrectly defined on
+  primitive projections (#4588)
+
+Plugin development tools
+- add a .merlin target to the makefile
+
+Various performance improvements (time, space used by .vo files)
+
+Other bugfixes
+
+- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
+- Added compatibility coercions from Specif.v which were present in Coq 8.4.
+- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
+- Allow to unset the refinement mode of Instance in ML
+- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
+- Add -compat 8.4 econstructor tactics, and tests
+- Add compatibility Nonrecursive Elimination Schemes
+- Fixing the "No applicable tactic" non informative error message regression on apply.
+- Univs: fix get_current_context (bug #4603, part I)
+- Fix a bug in Program coercion code
+- Fix handling of arity of definitional classes.
+- #4630: Some tactics are 20x slower in 8.5 than 8.4.
+- #4627: records with no declared arity can be template polymorphic.
+- #4623: set tactic too weak with universes (regression)
+- Fix incorrect behavior of CS resolution
+- #4591: Uncaught exception in directory browsing.
+- CoqIDE is more resilient to initialization errors.
+- #4614: "Fully check the document" is uninterruptable.
+- Try eta-expansion of records only on non-recursive ones
+- Fix bug when a sort is ascribed to a Record
+- Primitive projections: protect kernel from erroneous definitions.
+- Fixed bug #4533 with previous Keyed Unification commit
+- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
+- Fix strategy of Keyed Unification
+- #4608: Anomaly "output_value: abstract value (outside heap)".
+- #4607: do not read native code files if native compiler was disabled.
+- #4105: poor escaping in the protocol between CoqIDE and coqtop.
+- #4596: [rewrite] broke in the past few weeks.
+- #4533 (partial): respect declared global transparency of projections in unification.ml
+- #4544: Backtrack on using full betaiota reduction during keyed unification.
+- #4540: CoqIDE bottom progress bar does not update.
+- Fix regression from 8.4 in reflexivity
+- #4580: [Set Refine Instance Mode] also used for Program Instance.
+- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
+- STM: Print/Extraction have to be skipped if -quick
+- #4542: CoqIDE: STOP button also stops workers
+- STM: classify some variants of Instance as regular `Fork nodes.
+- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
+- Do not give a name to anonymous evars anymore. See bug #4547.
+- STM: always stock in vio files the first node (state) of a proof
+- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
+- Don't fail fatally if PATH is not set.
+- #4537: Coq 8.5 is slower in typeclass resolution.
+- #4522: Incorrect "Warning..." on windows.
+- #4373: coqdep does not know about .vio files.
+- #3826: "Incompatible module types" is uninformative.
+- #4495: Failed assertion in metasyntax.ml.
+- #4511: evar tactic can create non-typed evars.
+- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
+- #4519: oops, global shadowed local universe level bindings.
+- #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed.
+- #4548: Coqide crashes when going back one command
+
 Changes from V8.5beta3 to V8.5
 ==============================
 
diff --git a/configure.ml b/configure.ml
index b8bb650b1..80a776471 100644
--- a/configure.ml
+++ b/configure.ml
@@ -565,6 +565,12 @@ let check_camlp5_version () =
   | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
   | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
 
+let check_caml_version_for_camlp4 () =
+  if caml_version_nums = [4;1;0] && !Prefs.debug then
+    die ("Your version of OCaml is 4.01.0 which fails to compile Coq in -debug\n" ^
+            "mode with Camlp4. Remove -debug option or use a different version of OCaml\n" ^
+            "or use Camlp5.\n")
+
 let config_camlpX () =
   try
     if not !Prefs.usecamlp5 then raise NoCamlp5;
@@ -583,6 +589,7 @@ let config_camlpX () =
       let camlp4orf = which_camlpX "camlp4orf" in
       let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in
       let camlp4_version = List.nth (string_split ' ' version_line) 2 in
+      check_caml_version_for_camlp4 ();
       "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version
     with _ -> die "No Camlp4 installation found.\n"
 
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 077e2f0df..df5ee405f 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -406,8 +406,8 @@
 \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4
                                                  \,)\end{array}$}}
 %END LATEX
-%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
-%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
+%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}}
+%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}}
 
 \newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
                                                  \,)\end{array}$}}
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1554ee04d..b9c17d814 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -544,32 +544,109 @@ $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of param
     \def\colon{@{\hskip.5em:\hskip.5em}}
 
 The declaration for parameterized lists is:
+\begin{latexonly}
     \vskip.5em
 
-\ind{1}{\List:\Set\ra\Set}{\left[\begin{array}{r \colon l}
-                        \Nil & \forall A:\Set,\List~A \\
-                        \cons & \forall A:\Set, A \ra \List~A \ra \List~A
-                        \end{array}\right]}
+\ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r \colon l}
+                                      \Nil & \forall A:\Set,\List~A \\
+                                      \cons & \forall A:\Set, A \ra \List~A \ra \List~A
+                                   \end{array}
+                             \right]}
     \vskip.5em
-
-which corresponds to the result of the \Coq\ declaration:
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+  <tr style="vertical-align:middle">
+    <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+    <td style="width:20pt;text-align:center">[1]</td>
+    <td style="width:5pt;text-align:center">⎛<br>⎝</td>
+    <td style="width:120pt;text-align:center">[ <span style="font-family:monospace">list : Set → Set</span> ]</td>
+    <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+    <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+    <td>
+      <table style="border-spacing:0">
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">nil</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+          <td style="text-align:left;font-family:monospace">∀A : Set, list A</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">cons</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+          <td style="text-align:left;font-family:monospace">∀A : Set, A → list A → list A</td>
+        </tr>
+      </table>
+    </td>
+    <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+    <td style="width:5pt;text-align:center">⎞<br>⎠</td>
+  </tr>
+</table></pre>
+\end{rawhtml}
+\noindent which corresponds to the result of the \Coq\ declaration:
 \begin{coq_example*}
 Inductive list (A:Set) : Set :=
   | nil : list A
   | cons : A -> list A -> list A.
 \end{coq_example*}
 
-The declaration for a mutual inductive definition of forests and trees is:
+\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is:
+\begin{latexonly}
     \vskip.5em
-\ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
-      {\left[\begin{array}{r \colon l}
-            \node & \forest \ra \tree\\
-            \emptyf & \forest\\
-            \consf & \tree \ra \forest \ra \forest\\
-                      \end{array}\right]}
+\ind{~}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
+       {\left[\begin{array}{r \colon l}
+             \node & \forest \ra \tree\\
+             \emptyf & \forest\\
+             \consf & \tree \ra \forest \ra \forest\\
+                       \end{array}\right]}
     \vskip.5em
- 
-which corresponds to the result of the \Coq\ 
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+  <tr style="vertical-align:middle">
+    <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+    <td style="width:20pt;text-align:center">[1]</td>
+    <td style="width:5pt;text-align:center">⎛<br>⎜<br>⎝</td>
+    <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+    <td>
+      <table style="border-spacing:0">
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">tree</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">Set</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">forest</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">Set</td>
+        </tr>
+      </table>
+    </td>
+    <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+    <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+    <td style="width:10pt;text-align:center">⎡<br>⎢<br>⎣</td>
+    <td>
+      <table style="border-spacing:0">
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">node</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">forest → tree</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">emptyf</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">forest</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">consf</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">tree → forest → forest</td>
+        </tr>
+      </table>
+    </td>
+    <td style="width:10pt;text-align:center">⎤<br>⎥<br>⎦</td>
+    <td style="width:5pt;text-align:center">⎞<br>⎟<br>⎠</td>
+  </tr>
+</table></pre>
+\end{rawhtml}
+\noindent which corresponds to the result of the \Coq\
 declaration:
 \begin{coq_example*}
 Inductive tree : Set :=
@@ -579,7 +656,8 @@ with forest : Set :=
   | consf : tree -> forest -> forest.
 \end{coq_example*}
 
-The declaration for a mutual inductive definition of even and odd is:
+\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is:
+\begin{latexonly}
     \newcommand\GammaI{\left[\begin{array}{r \colon l}
                         \even & \nat\ra\Prop \\
                         \odd & \nat\ra\Prop
@@ -594,7 +672,55 @@ The declaration for a mutual inductive definition of even and odd is:
     \vskip.5em
     \ind{1}{\GammaI}{\GammaC}
     \vskip.5em
-which corresponds to the result of the \Coq\ 
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+  <tr style="vertical-align:middle">
+    <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+    <td style="width:20pt;text-align:center">[1]</td>
+    <td style="width:5pt;text-align:center">⎛<br>⎜<br>⎝</td>
+    <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+    <td>
+      <table style="border-spacing:0">
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">even</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">nat → Prop</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">odd</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">nat → Prop</td>
+        </tr>
+      </table>
+    </td>
+    <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+    <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+    <td style="width:10pt;text-align:center">⎡<br>⎢<br>⎣</td>
+    <td>
+      <table style="border-spacing:0">
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">even_O</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">even O</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">even_S</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">∀n : nat, odd n → even (S n)</td>
+        </tr>
+        <tr>
+          <td style="width:20pt;text-align:right;font-family:monospace">odd_S</td>
+          <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+          <td style="text-align:left;font-family:monospace">∀n : nat, even n → odd (S n)</td>
+        </tr>
+      </table>
+    </td>
+    <td style="width:10pt;text-align:center">⎤<br>⎥<br>⎦</td>
+    <td style="width:5pt;text-align:center">⎞<br>⎟<br>⎠</td>
+  </tr>
+</table></pre>
+\end{rawhtml}
+\noindent which corresponds to the result of the \Coq\
 declaration:
 \begin{coq_example*}
 Inductive even : nat -> Prop :=
@@ -610,9 +736,9 @@ contains an inductive declaration.
 
 \begin{description}
 \item[Ind]  \index{Typing rules!Ind}
-  \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
+  \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
 \item[Constr]  \index{Typing rules!Constr}
-  \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
+  \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
 \end{description}
 
 \begin{latexonly}%
@@ -726,19 +852,16 @@ any $u_i$
 the type $V$ satisfies the nested positivity condition for $X$
 \end{itemize}
 
-%% \begin{latexonly}%
-   \newcommand\vv{\textSFxi}    % │
-   \newcommand\hh{\textSFx}     %   ─
-   \newcommand\vh{\textSFviii}  % ├
-   \newcommand\hv{\textSFii}    %   └
-   \newlength\framecharacterwidth
-   \settowidth\framecharacterwidth{\hh}
-   \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
-   \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
-%%   \def\captionstrut{\vbox to 1.5em{}}
+\newcommand\vv{\textSFxi}    % │
+\newcommand\hh{\textSFx}     %   ─
+\newcommand\vh{\textSFviii}  % ├
+\newcommand\hv{\textSFii}    %   └
+\newlength\framecharacterwidth
+\settowidth\framecharacterwidth{\hh}
+\newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
+\newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
 
-%%   \begin{figure}[H]
-For instance, if one considers the type
+\noindent For instance, if one considers the type
 
 \begin{verbatim}
 Inductive tree (A:Type) : Type :=
@@ -746,29 +869,49 @@ Inductive tree (A:Type) : Type :=
  | node : A -> (nat -> tree A) -> tree A
 \end{verbatim}
 
-Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$
-
+\begin{latexonly}
+\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\
 \noindent
-    \ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
-    \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
-    \ws\ws\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
-    \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
-    \ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
-%%     \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$}
-%%   \end{figure}
-%% \end{latexonly}%
+\ws\ws\vv\\
+\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
+\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
+\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
+\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
+\ws\ws\vv\\
+\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
+\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
+\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
+\end{latexonly}
+\begin{rawhtml}
+<pre>
+<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">list A</span> satisfies the nested positivity condition for <span style="font-family:monospace">list</span></span>
+  │
+  ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span>:</span>
+  │    <span style="font-family:serif">Type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">list</span></span>
+  │    <span style="font-family:serif">because <span style="font-family:monospace">list</span> does not appear in any (real) arguments of the type of that constructor</span>
+  │    <span style="font-family:serif">(primarily because list does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span>
+  │
+  ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span>:</span>
+       <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span></span>
+       <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">list</span> because:</span>
+       │
+       ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+       │
+       ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+       │
+       ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 4)</span></span>
+       │
+       ╰─ <span style="font-family:serif"><span style="font-family:monospace">list</span> satisfies the positivity condition for <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 1)</span></span>
+</pre>
+\end{rawhtml}
 
 \paragraph{Correctness rules.}
 We shall now describe the rules allowing the introduction of a new
@@ -783,7 +926,7 @@ inductive definition.
 \inference{
   \frac{
   (\WTE{\Gamma_P}{A_j}{s'_j})_{j=1\ldots  k}
-  ~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots  n}
+  ~~~~~~~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots  n}
 }
   {\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
 provided that the following side conditions hold:
@@ -811,23 +954,23 @@ inductive definition.
 The following declaration introduces the second-order existential
 quantifier $\exists X.P(X)$.
 \begin{coq_example*}
-Inductive exProp (P:Prop->Prop) : Prop 
-  := exP_intro : forall X:Prop, P X -> exProp P.
+Inductive exProp (P:Prop->Prop) : Prop :=
+  exP_intro : forall X:Prop, P X -> exProp P.
 \end{coq_example*}
 The same definition on \Set{} is not allowed and fails:
 % (********** The following is not correct and should produce **********)
 % (*** Error: Large non-propositional inductive types must be in Type***)
 \begin{coq_example}
-Fail Inductive exSet (P:Set->Prop) : Set
-  := exS_intro : forall X:Set, P X -> exSet P.
+Fail Inductive exSet (P:Set->Prop) : Set :=
+  exS_intro : forall X:Set, P X -> exSet P.
 \end{coq_example}
 It is possible to declare the same inductive definition in the
 universe \Type. 
 The \texttt{exType} inductive definition has type  $(\Type_i \ra\Prop)\ra
 \Type_j$ with the constraint that the parameter \texttt{X} of \texttt{exT\_intro} has type $\Type_k$ with $k<j$ and $k\leq i$.
 \begin{coq_example*}
-Inductive exType (P:Type->Prop) : Type
-  := exT_intro : forall X:Type, P X -> exType P.
+Inductive exType (P:Type->Prop) : Type :=
+  exT_intro : forall X:Type, P X -> exType P.
 \end{coq_example*}
 %We shall assume for the following definitions that, if necessary, we
 %annotated the type of constructors such that we know if the argument
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6561000c4..5ceb25a8f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -854,15 +854,21 @@ let rec match_ inner u alp metas sigma a1 a2 =
      otherwise how to ensure it corresponds to a well-typed eta-expansion;
      we make an exception for types which are metavariables: this is useful e.g.
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
-  | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner ->
-      let id' = Namegen.next_ident_away id (free_glob_vars b1) in
+  | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+      let avoid =
+        free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in
+      let id' = Namegen.next_ident_away id avoid in
       let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
       let sigma = match t2 with
       | NHole _ -> sigma
       | NVar id2 -> bind_term_env alp sigma id2 t1
       | _ -> assert false in
-      match_in u alp metas (add_bindinglist_env sigma id [(Name id',Explicit,None,t1)])
-       (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
+      let (alp,sigma) =
+        if is_bindinglist_meta id metas then
+          alp, add_bindinglist_env sigma id [(Name id',Explicit,None,t1)]
+        else
+          match_names metas (alp,sigma) (Name id') na in
+      match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
 
   | (GRec _ | GEvar _), _
   | _,_ -> raise No_match
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index c482c694e..a165e32bb 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -193,7 +193,11 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   let entry_create = Entry.create
   let entry_parse e p =
     try Entry.parse e p
-    with Exc_located (loc,e) -> Loc.raise (to_coqloc loc) e
+    with Exc_located (loc,e) ->
+      let loc' = Loc.get_loc (Exninfo.info e) in
+      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
+      Loc.raise loc e
+
 IFDEF CAMLP5_6_02_1 THEN
   let entry_print ft x = Entry.print ft x
 ELSE
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 9a1a4aa01..c9e8eac0c 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -46,7 +46,7 @@ Extract Constant Pos.max => "Big.max".
 Extract Constant Pos.compare =>
  "fun x y -> Big.compare_case Eq Lt Gt x y".
 Extract Constant Pos.compare_cont =>
- "fun x y c -> Big.compare_case c Lt Gt x y".
+ "fun c x y -> Big.compare_case c Lt Gt x y".
 
 Extract Constant N.add => "Big.add".
 Extract Constant N.succ => "Big.succ".
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index c9860864a..e3b6fb08a 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -266,7 +266,7 @@ let add_name_to_ids set na =
     | Anonymous -> set
     | Name id -> Id.Set.add id set
 
-let free_glob_vars  =
+let free_glob_vars =
   let rec vars bounded vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
     | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
@@ -324,6 +324,16 @@ let free_glob_vars  =
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
 
+let glob_visible_short_qualid c =
+  let rec aux acc = function
+    | GRef (_,c,_) ->
+        let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
+        let dir,id = Libnames.repr_qualid  qualid in
+        if DirPath.is_empty dir then id :: acc else acc
+    | c ->
+        fold_glob_constr aux acc c
+  in aux [] c
+
 let add_and_check_ident id set =
   if Id.Set.mem id set then
     Pp.(msg_warning
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 45444234a..e0a2de032 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -40,6 +40,7 @@ val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
 val bound_glob_vars : glob_constr -> Id.Set.t
 val loc_of_glob_constr : glob_constr -> Loc.t
+val glob_visible_short_qualid : glob_constr -> Id.t list
 
 (** [map_pattern_binders f m c] applies [f] to all the binding names
     in a pattern-matching expression ({!Glob_term.GCases}) represented
diff --git a/stm/stm.ml b/stm/stm.ml
index 92032e9bc..b25e88812 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -8,8 +8,8 @@
 
 let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
 
-let prerr_endline s = if false then begin pr_err s end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if false then begin pr_err (s ()) end else ()
+let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
 
 open Vernacexpr
 open Errors
@@ -104,11 +104,11 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
     | _ -> false in
   if internal_command expr then begin
-    prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
+    prerr_endline (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr))
   end else begin
     set_id_for_feedback ?route (Feedback.State id);
     Aux_file.record_in_aux_set_at loc;
-    prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
+    prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr));
     try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
     with e ->
       let e = Errors.push e in
@@ -478,7 +478,7 @@ end = struct (* {{{ *)
         let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
-        prerr_endline ("mode:" ^ mode);
+        prerr_endline (fun () -> "mode:" ^ mode);
         Proof_global.activate_proof_mode mode
       with Failure _ ->
         checkout Branch.master;
@@ -743,7 +743,7 @@ end = struct (* {{{ *)
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
     try
-      prerr_endline("defining "^str_id^" (cache="^
+      prerr_endline (fun () -> "defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
@@ -751,7 +751,7 @@ end = struct (* {{{ *)
       fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
-      prerr_endline ("setting cur id to "^str_id);
+      prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
         Hooks.(call state_computed id ~in_cache:false);
@@ -1133,8 +1133,8 @@ end = struct (* {{{ *)
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        prerr_endline "failed with the following exception:";
-        prerr_endline (string_of_ppcmds e_msg);
+        prerr_endline (fun () -> "failed with the following exception:");
+        prerr_endline (fun () -> string_of_ppcmds e_msg);
         let e_safe_states = List.filter State.is_cached my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
   
@@ -1400,7 +1400,7 @@ end = struct (* {{{ *)
              | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
-    prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
     reqs
 
   let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1568,7 +1568,7 @@ end = struct (* {{{ *)
             with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
           if Future.is_over f then
             let pt, uc = Future.join f in
-            prerr_endline (string_of_ppcmds(hov 0 (
+            prerr_endline (fun () -> string_of_ppcmds(hov 0 (
               str"g=" ++ str gid ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
               str"uc=" ++ Evd.pr_evar_universe_context uc)));
@@ -1680,7 +1680,7 @@ let delegate name =
               || !Flags.async_proofs_full
  
 let collect_proof keep cur hd brkind id =
- prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
  let name = function
    | [] -> no_name
@@ -1781,7 +1781,7 @@ let string_of_reason = function
   | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
   | `Unknown -> "unsupported case"
 
-let log_string s = prerr_debug ("STM: " ^ s)
+let log_string s = prerr_debug (fun () -> "STM: " ^ s)
 let log_processing_async id name = log_string Printf.(sprintf
   "%s: proof %s: asynch" (Stateid.to_string id) name
 )
@@ -1803,17 +1803,17 @@ let known_state ?(redefine_qed=false) ~cache id =
     Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
   in
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
-    prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
+    prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
     reach id;
     cherry_pick_non_pstate ()) id
 
   (* traverses the dag backward from nodes being already calculated *)
   and reach ?(redefine_qed=false) ?(cache=cache) id =
-    prerr_endline ("reaching: " ^ Stateid.to_string id);
+    prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
       State.install_cached id;
       Hooks.(call state_computed id ~in_cache:true);
-      prerr_endline ("reached (cache)")
+      prerr_endline (fun () -> "reached (cache)")
     end else
     let step, cache_step, feedback_processed =
       let view = VCS.visit id in
@@ -1951,7 +1951,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       else cache_step in
     State.define
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    prerr_endline ("reached: "^ Stateid.to_string id) in
+    prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
 end (* }}} *)
@@ -1966,7 +1966,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline "Initializing workers";
+    prerr_endline (fun () -> "Initializing workers");
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
@@ -2018,9 +2018,9 @@ let rec join_admitted_proofs id =
 let join () =
   finish ();
   wait ();
-  prerr_endline "Joining the environment";
+  prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
-  prerr_endline "Joining Admitted proofs";
+  prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
   VCS.print ()
@@ -2096,7 +2096,7 @@ let handle_failure (e, info) vcs tty =
       anomaly(str"error with no safe_id attached:" ++ spc() ++
         Errors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
-      prerr_endline ("Failed at state " ^ Stateid.to_string id);
+      prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
       if tty && interactive () = `Yes then begin
         (* We stay on a valid state *)
@@ -2121,13 +2121,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
   let warn_if_pos a b =
     if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
   let v, x = expr, { verbose = verbose; loc; expr } in
-  prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
   let vcs = VCS.backup () in
   try
     let head = VCS.current_branch () in
     VCS.checkout head;
     let rc = begin
-      prerr_endline ("  classified as: " ^ string_of_vernac_classification c);
+      prerr_endline (fun () -> "  classified as: " ^ string_of_vernac_classification c);
       match c with
       (* PG stuff *)    
       | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
@@ -2163,7 +2163,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
-          prerr_endline ("undo to state " ^ Stateid.to_string id);
+          prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2251,7 +2251,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
           VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
-          VCS.propagate_sideff (Some x);
+	  let replay = match x.expr with
+	    | VernacDefinition(_, _, DefineBody _) -> None
+	    | _ -> Some x
+	  in
+	  VCS.propagate_sideff replay;
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
 
@@ -2298,7 +2302,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
               expr = VernacShow (ShowGoal OpenSubgoals) }
       | _ -> ()
     end;
-    prerr_endline "processed }}}";
+    prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
   with e ->
@@ -2476,7 +2480,7 @@ let edit_at id =
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
           Errors.print_no_report e)
     | Some (_, id) ->
-        prerr_endline ("Failed at state " ^ Stateid.to_string id);
+        prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         iraise (e, info)
diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v
new file mode 100644
index 000000000..e7567623a
--- /dev/null
+++ b/test-suite/bugs/closed/4603.v
@@ -0,0 +1,10 @@
+Axiom A : Type.
+
+Goal True. exact I.
+Check (fun P => P A).
+Abort.
+
+Goal True.
+Definition foo (A : Type) : Prop:= True. 
+  set (x:=foo). split.
+Qed.
\ No newline at end of file
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 58ec1de56..6ff1d3837 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -50,3 +50,7 @@ end
      : nat -> nat
 # _ : nat => 2
      : nat -> nat
+# x : nat => # H : x <= 0 => exist (le x) 0 H
+     : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
+exist (Q x) y conj
+     : {x0 : A | Q x x0}
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e53c94ef0..4e0d135d7 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -68,6 +68,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
 
 (* In practice, only the printing rule is used here *)
 (* Note: does not work for pattern *)
+Module A.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
 Check fun f x => f x + S x.
 
@@ -77,6 +78,7 @@ Notation plus2 n := (S (S n)).
 (* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
 Print plus2.
 Check fun n => match n with list1 => 0 | _ => 2 end.
+End A.
 
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder
@@ -98,3 +100,9 @@ Notation "#  x : T => t" := (fun x : T => t)
 
 Check # x : nat => x.
 Check # _ : nat => 2.
+
+(* Check bug 4677 *)
+Check fun x (H:le x 0) => exist (le x) 0 H.
+
+Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
+Check (exist (Q x) y conj).
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 12869e3d5..fb57e55ef 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -37,8 +37,8 @@ open Sigma.Notations
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
-let prerr_endline =
-  if debug then prerr_endline else fun _ -> ()
+let prerr_endline x =
+  if debug then prerr_endline (x ()) else ()
 
 (* Misc *)
 
@@ -1732,7 +1732,7 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~loc locality poly c =
-  prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+  prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
   (* Done later in this file *)
   | VernacLoad _ -> assert false