14 files changed, 67 insertions, 35 deletions
diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh
new file mode 100644
index 0000000000..18a295cdbb
--- /dev/null
+++ b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then
+
+    equations_CI_REF=more-delta-in-termination-checking
+    equations_CI_GITURL=https://github.com/gares/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh
new file mode 100644
index 0000000000..ccb3498764
--- /dev/null
+++ b/dev/ci/user-overlays/09678-printed-by-env.sh
@@ -0,0 +1,14 @@
+
+if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then
+    elpi_CI_REF=printed-by-env
+    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    equations_CI_REF=printed-by-env
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+    ltac2_CI_REF=printed-by-env
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    quickchick_CI_REF=printed-by-env
+    quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick
+fi
diff --git a/dev/doc/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY
index a81afca32d..a81afca32d 100644
--- a/dev/doc/COMPATIBILITY
+++ b/dev/doc/archive/COMPATIBILITY
diff --git a/dev/doc/extensions.txt b/dev/doc/archive/extensions.txt
index 075496db7c..36d63029f1 100644
--- a/dev/doc/extensions.txt
+++ b/dev/doc/archive/extensions.txt
@@ -16,4 +16,3 @@ Exemple de l'ajout de l'entrée "clause":
   faut rejouter clause dans le GLOBAL du GEXTEND
 
 - seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
-
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex
index 337b9226df..0b0811d81b 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/archive/naming-conventions.tex
@@ -133,7 +133,7 @@ has name \texttt{D\_integral}, then
 \end{quote}
 will have name \texttt{D\_integral\_inf}.
 
-As an exception, decidability statements, such as 
+As an exception, decidability statements, such as
 \begin{quote}
 \begin{tt}
 {forall x y, \{x = y\} + \{x <> y\}}
@@ -284,7 +284,7 @@ If the conclusion is in the other way than listed below, add suffix
 
 \itemrule{Nilpotency of element elt wrt a ring D with additive neutral
 element {\zero} and multiplicative binary operator
-{\op}}{Delt\_nilpotent} 
+{\op}}{Delt\_nilpotent}
 {op elt elt = zero}
 
   Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''.
@@ -487,7 +487,7 @@ binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism}
 {forall x y:D, phi (op x y) <-> rel (phi x) (phi y)}
 
 Remark: If the operator and the relation have similar name, one uses
-\texttt{phi\_op}. 
+\texttt{phi\_op}.
 
 Question: How to name each direction? (add \_elim for -> and \_intro
 for <- ?? -- as done in Bool.v ??)
diff --git a/dev/doc/newsyntax.tex b/dev/doc/archive/newsyntax.tex
index d1986fa0d1..71e964bcc9 100644
--- a/dev/doc/newsyntax.tex
+++ b/dev/doc/archive/newsyntax.tex
@@ -50,7 +50,7 @@
 La réflexion de la rénovation de la syntaxe des tactiques n'est pas
 encore aussi poussée que pour les termes (section~\ref{constrsyntax}),
 mais cette section vise à énoncer les quelques principes que l'on
-souhaite suivre. 
+souhaite suivre.
 
 \begin{itemize}
 \item Réutiliser les mots-clés de la syntaxe des termes (i.e. en
@@ -612,7 +612,7 @@ Fixpoint plus n m : nat {struct n} :=
 \subsection{Questions ouvertes}
 
 Voici les points sur lesquels la discussion est particulièrement
-ouverte: 
+ouverte:
 \begin{itemize}
 \item choix d'autres symboles pour les quantificateurs \TERM{!} et
   \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!}
diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/archive/notes-on-conversion.v
index a81f170c63..a78ecd181a 100644
--- a/dev/doc/notes-on-conversion.v
+++ b/dev/doc/archive/notes-on-conversion.v
@@ -69,5 +69,3 @@ it is not convertible.
 The only hope to improve this problem is to observe that S' hides
 (behind two indirections) a Setoid constructor. This could be the
 argument to solve the problem.
-
-
diff --git a/dev/doc/old_svn_branches.txt b/dev/doc/archive/old_svn_branches.txt
index ee56ee24e9..ee56ee24e9 100644
--- a/dev/doc/old_svn_branches.txt
+++ b/dev/doc/archive/old_svn_branches.txt
diff --git a/dev/doc/perf-analysis b/dev/doc/archive/perf-analysis
index ac54fa6f73..ac54fa6f73 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/archive/perf-analysis
diff --git a/dev/doc/versions-history.tex b/dev/doc/archive/versions-history.tex
index 1c4913d201..25dabad497 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/archive/versions-history.tex
@@ -135,7 +135,7 @@ Coq V5.8.3& released 6 December 1993 % Announce on coq-club
 
  & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\
 
-Coq V5.9 alpha& 7 July 1993 & 
+Coq V5.9 alpha& 7 July 1993 &
 experimental version based on evars refinement \\
               & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\
               & & version), not released\\
@@ -159,7 +159,7 @@ Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\
 \begin{tabular}{l|l|l}
 version & date & comments \\
 \hline
-Coq V5.10 ``Murthy'' & 22 January 1994 & 
+Coq V5.10 ``Murthy'' & 22 January 1994 &
 introduction of the ``DOPN'' structure\\
  & & \feature{eapply/prolog} tactics\\
  & & private use of cvs on madiran.inria.fr\\
@@ -179,7 +179,7 @@ Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\
 
 Coq V5.10.9& announced on 17 August 1994 &
  % Announced by Catherine Parent on coqdev
- % Version avec une copie de THEORIES pour les inductifs mutuels 
+ % Version avec une copie de THEORIES pour les inductifs mutuels
  \\
 
 Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\
@@ -192,7 +192,7 @@ Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\
 
 Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\
 
-Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW 
+Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW
 
 Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
   & & MS-DOS version released on 30 October 1995\\
@@ -203,7 +203,7 @@ Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
 
 Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\
   % Announce on coq-club by BW
-  % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive 
+  % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive
   & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW
 
 Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\
@@ -434,7 +434,7 @@ evars-based experimentation \\
  & & to Coq V5.7, version from October/November
 1992\\
 
-CtCoq & released 25 October 1995 & first beta-version  \\ % Announce on coq-club by Janet  
+CtCoq & released 25 October 1995 & first beta-version  \\ % Announce on coq-club by Janet
 
 Proto with explicit substitutions & 1997 &\\
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index d515ec30e8..416253fad1 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -54,6 +54,15 @@ Macros:
   where `atts : Vernacexpr.vernac_flags` was bound in the expression
   and had to be manually parsed.
 
+- `PRINTED BY` now binds `env` and `sigma`, and expects printers which take
+  as parameters term printers parametrized by an environment and an `evar_map`.
+
+Printers
+
+- `Ppconstr.pr_constr_expr`, `Ppconstr.lconstr_expr`,
+  `Ppconstr.pr_constr_pattern_expr` and `Ppconstr.pr_lconstr_pattern_expr`
+  now all take an environment and an `evar_map`.
+
 Libobject
 
 - A Higher-level API for objects with fixed scope was introduced. It supports the following kinds of objects:
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 8d78559c0d..c0a5b9095c 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -63,8 +63,8 @@ Typing constructions
   impacted coqchk versions: ?
   fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
   found by: Georgi Guninski
-  exploit: test-suite/bugs/closed/4294.v
-  GH issue number: #4294
+  exploit: test-suite/failure/prop_set_proof_irrelevance.v
+  GH issue number: none?
   risk: ?
 
 Module system
@@ -77,7 +77,7 @@ Module system
   impacted coqchk versions: ?
   fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau)
   found by: Dénès
-  exploit: test-suite/bugs/closed/4294.v
+  exploit: test-suite/bugs/closed/bug_4294.v
   GH issue number: #4294
   risk: ?
 
@@ -105,7 +105,7 @@ Universes
   impacted coqchk versions: ?
   fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), 
   found by: Barras
-  exploit: test-suite/failure/inductive4.v
+  exploit: test-suite/failure/inductive.v
   GH issue number: none
   risk: unlikely to be activated by chance
 
@@ -141,7 +141,7 @@ Primitive projections
   impacted coqchk versions: ?
   fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès)
   found by: Dénès exploiting bug #4588
-  exploit: test-suite/bugs/closed/4588.v
+  exploit: test-suite/bugs/closed/bug_4588.v
   GH issue number: #4588
   risk: ?
 
@@ -167,7 +167,7 @@ Conversion machines
   impacted coqchk versions: none (no virtual machine in coqchk)
   fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport)
   found by: Dénès, Pédrot
-  exploit: test-suite/failure/vm-bug4157.v
+  exploit: test-suite/bugs/closed/bug_4157.v
   GH issue number: #4157
   risk: 
 
@@ -179,7 +179,7 @@ Conversion machines
   impacted coqchk versions: none (no virtual machine in coqchk)
   fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport)
   found by: Dénès
-  exploit: test-suite/bugs/closed/6677.v
+  exploit: test-suite/bugs/closed/bug_6677.v
   GH issue number: #6677
   risk: 
 
@@ -203,7 +203,7 @@ Conversion machines
   impacted coqchk versions: none (no native computation in coqchk)
   fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), 
   found by: Letouzey, Dénès
-  exploit: lost?
+  exploit: see commit message for 244d7a9aa
   GH issue number: ?
   risk: 
 
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 9864fd4d69..1ec8251f66 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -30,13 +30,15 @@ while [[ $# -gt 0 ]]; do
     esac
 done
 
-if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
+MASTER=origin/master
+
+if ! git log $MASTER --grep "Merge PR #$PRNUM" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
     exit 1
 fi
 
-SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?")
-git log master --grep "Merge PR #${PRNUM}" --format="%GG"
+SIGNATURE_STATUS=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%G?")
+git log $MASTER --grep "Merge PR #$PRNUM" --format="%GG"
 if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
     echo
     read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
@@ -47,10 +49,18 @@ if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
 fi
 
 BRANCH=backport-pr-${PRNUM}
-RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
-MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
+RANGE=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%P" | sed 's/ /../')
+MESSAGE=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%s" | sed 's/Merge/Backport/')
 
-if git checkout -b "${BRANCH}"; then
+if [[ "$(git rev-parse --abbrev-ref HEAD)" == "$BRANCH" ]]; then
+
+    if ! git cherry-pick --continue; then
+        echo "Please fix the conflicts, then relaunch the script."
+        exit 1
+    fi
+    git checkout -
+
+elif git checkout -b "$BRANCH"; then
 
     if ! git cherry-pick -x "${RANGE}"; then
         if [[ "$NO_CONFLICTS" == "true" ]]; then
@@ -61,12 +71,8 @@ if git checkout -b "${BRANCH}"; then
             git branch -d "$BRANCH"
             exit 1
         fi
-        echo "Please fix the conflicts, then exit."
-        bash
-        while ! git cherry-pick --continue; do
-            echo "Please fix the conflicts, then exit."
-            bash
-        done
+        echo "Please fix the conflicts, then relaunch the script."
+        exit 1
     fi
     git checkout -
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0fbb0634a5..499bbba37e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -72,7 +72,7 @@ let pr_econstr t =
   Printer.pr_econstr_env env sigma t
 let ppconstr x = pp (pr_constr x)
 let ppeconstr x = pp (pr_econstr x)
-let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
+let ppconstr_expr x = let sigma,env = Pfedit.get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x)
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))