10 files changed, 103 insertions, 22 deletions
diff --git a/dev/README b/dev/README
index b446c3e974..6b83579def 100644
--- a/dev/README
+++ b/dev/README
@@ -1,4 +1,4 @@
-This directory contains informations and tools to help developing the
+This directory contains information and tools to help develop the
                              Coq system
                        ======================
 
@@ -6,30 +6,30 @@ This directory contains informations and tools to help developing the
 Debugging and profiling (in current directory - see doc/debugging.txt)
 -----------------------
 
-ocamldebug-coq: to launch ocaml debugger
+ocamldebug-coq: to launch ocaml debugger (generated by the configure script)
 
-db:      to install pretty-printers from ocaml debugger
-base_db: to install raw pretty-printers from ocaml debugger
+db:           to install pretty-printers from ocaml debugger
+base_db:      to install raw pretty-printers from ocaml debugger
 
-include:      to install pretty-printers from ocaml toplevel
+include:      to install pretty-printers from ocaml toplevel (use with the coq Drop command)
 base_include: to install raw pretty-printers from ocaml toplevel
 
-vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging
+vm_printers.ml, top_printers.ml: ML pretty-printers for debugging
 
 
-Miscellaneous informations about the code (directory doc)
+Miscellaneous information about the code (directory doc)
 -----------------------------------------
 
-changes.txt:   (partial) per-version summary of the evolutions of Coq ML source
-style.txt:     a few style recommendations for writing Coq ML files
-debugging.txt: help for debugging or profiling
-universes.txt: help to debug universes
-translate.txt: help to use coq translator
+changes.md:     (partial) per-version summary of the evolution of Coq ML source
+style.txt:      a few style recommendations for writing Coq ML files
+debugging.md:   help for debugging or profiling
+universes.txt:  help for debugging universes
+translate.txt:  help for using coq translator
 extensions.txt: some help about TACTIC EXTEND
 
-header:        standard header for Coq ML files
-perf-analysis: analysis of perfs measured on the compilation of user contribs
-cic.dtd:       official dtd of the calc. of ind. constr. for im/ex-portation
+header:         standard header for Coq ML files
+perf-analysis:  analysis of perfs measured on the compilation of user contribs
+cic.dtd:        official dtd of the calc. of ind. constr. for im/ex-portation
 
 
 Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index cfcc09b327..dc33838f1e 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -25,4 +25,4 @@ mkdir -p _build
 # Temporary countermeasure to hdiutil error 5341
 # head -c9703424 /dev/urandom > $DMGDIR/.padding
 
-hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg
+hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
index 48f1d3759b..2c2f0fa47c 100644
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -15,7 +15,7 @@
 SetCompressor lzma
 
 !define MY_PRODUCT "Coq" ;Define your own software name here
-!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
+!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe"
 
 !include "MUI2.nsh"
 !include "FileAssociation.nsh"
diff --git a/dev/ci/README.md b/dev/ci/README.md
index f4423558cc..bb13587e94 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external
 development repositories, merge the latter first (if the fixes are
 backward-compatible), drop the overlay commit and merge the PR on Coq then.
 
+See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
+
 
 Travis specific information
 ---------------------------
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index 72ee89962c..dec6f0d182 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -25,7 +25,7 @@ if %USEOPAM% == false (
     -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
     -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
   copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
-  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+  7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
 )
 
 if %USEOPAM% == true (
diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
new file mode 100644
index 0000000000..78789a6fc5
--- /dev/null
+++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then
+    HoTT_CI_BRANCH=check-poly-effects
+    HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git
+fi
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index fa145d498a..fd3cbd1bc3 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism
   printers too.
 
 
-Debugging from Caml debugger
-============================
+Debugging with ocamldebug from Emacs
+====================================
 
    Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
    Coq must be configured with `-local` (`./configure -local`) and the
@@ -59,6 +59,29 @@ Debugging from Caml debugger
      from the debugger. If this happens, unset the variable, re-start Emacs, and 
      run the debugger again.
 
+Debugging with ocamldebug from the command line
+===============================================
+
+In the `coq` directory:
+1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq.
+2. Run `make` (to compile the .v files)
+3. Run `make byte`
+4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH.
+   Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH.  (The
+   CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.)
+5. Run `dev/ocamldebug-coq bin/coqtop.byte`  (on Cygwin/Windows, use `... bin/coqtop.byte.exe`)
+6. Enter `source db` to load printers
+7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc.
+8. See the ocamldebug manual for more information.  A few points:
+   - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml).
+     `break` can be abbreviated as `b`.
+   - `backtrace` or `bt` to see the call stack
+   - `step` or `s` goes into called functions; `next` or `n` skips over them
+   - `list` or `li` shows the code just before and after the current stack frame
+   - `print <var>` or `p <var>` to see the value of a variable
+Note that `make byte` doesn't recompile .v files.  `make` recompiles all of them if there
+are changes in any .ml file--safer but much slower.
+
 Global gprof-based profiling
 ============================
 
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 80da845174..f48013cf2e 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -13,7 +13,7 @@ SetCompressor lzma
 
 !define MY_PRODUCT "Coq" ;Define your own software name here
 !define COQ_SRC_PATH "..\.."
-!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
+!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe"
 
 !include "MUI2.nsh"
 !include "FileAssociation.nsh"
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 4c4dbe1e97..d7acf01f1d 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,10 +1,11 @@
 #!/usr/bin/env bash
 
-# Usage: dev/tools/backport-pr.sh <PR number>
+# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
 
 set -e
 
 PRNUM=$1
+OPTION=$2
 
 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
@@ -49,6 +50,10 @@ else
 
 fi
 
+if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+    exit 0
+fi
+
 git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
 git branch -d ${BRANCH}
 
diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
new file mode 100755
index 0000000000..beb26d9104
--- /dev/null
+++ b/dev/tools/github-check-prs.py
@@ -0,0 +1,47 @@
+#!/usr/bin/env python3
+
+# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance
+# debian package: python3-github
+# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py
+from github import Github
+import argparse
+
+REPO = "coq/coq"
+REBASE_LABEL="needs: rebase"
+
+parser = argparse.ArgumentParser()
+parser.add_argument("--token-file", type=argparse.FileType('r'))
+args = parser.parse_args()
+
+if args.token_file is None:
+    token = input("Github access token: ").strip()
+else:
+    token = args.token_file.read().rstrip("\n")
+    args.token_file.close()
+
+if token == "":
+    print ("Warning: using the GitHub API without a token")
+    print ("We may run into rate limit issues")
+    g = Github()
+else:
+    g = Github(token)
+
+repo = g.get_repo(REPO)
+
+for pull in repo.get_pulls():
+    # if conflicts then dirty
+    # otherwise blocked (because I have no rights)
+    dirty = pull.mergeable_state == "dirty"
+    labelled = False
+    for label in repo.get_issue(pull.number).get_labels():
+        if label.name == REBASE_LABEL:
+            labelled = True
+    if labelled and not dirty:
+        print ("PR #" + str(pull.number) + " is not dirty but is labelled")
+        print ("("+ pull.html_url +")")
+    elif dirty and not labelled:
+        print ("PR #" + str(pull.number) + " is dirty and not labelled")
+        print ("("+ pull.html_url +")")
+    else:
+        # give some feedback so the user can see we didn't crash
+        print ("PR #" + str(pull.number) + " OK")