5 files changed, 121 insertions, 5 deletions
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 5bfc408e96..5760fbafb0 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -8,6 +8,6 @@ VST_CI_DIR=${CI_BUILD_DIR}/VST
 # opam install -j ${NJOBS} -y menhir
 git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
 
-# Targets are: msl veric floyd
+# Targets are: msl veric floyd progs , we remove progs to save time
 # Patch to avoid the upper version limit
-( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true )
+( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd )
diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
new file mode 100644
index 0000000000..5c4dd1324f
--- /dev/null
+++ b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
@@ -0,0 +1,9 @@
+if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then
+    formal_topology_CI_BRANCH=ci
+    formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git
+
+    HoTT_CI_BRANCH=coq-pr-1033
+    HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git
+
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
+fi
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
new file mode 100755
index 0000000000..bc6ee31916
--- /dev/null
+++ b/dev/tools/backport-pr.sh
@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+
+# Usage: git-backport <PR number>
+
+set -e
+
+PRNUM=$1
+
+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"
+if [[ "${SIGNATURE_STATUS}" != "G" ]]; then
+    echo
+    read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+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/')
+
+if git checkout -b ${BRANCH}; then
+
+    if ! git cherry-pick -x ${RANGE}; then
+        echo "Please fix the conflicts, then exit."
+        bash
+        while ! git cherry-pick --continue; do
+            echo "Please fix the conflicts, then exit."
+            bash
+        done
+    fi
+    git checkout -
+
+else
+
+    echo
+    read -p "Skip directly to merging phase? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+
+fi
+
+git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
+git branch -d ${BRANCH}
+
+# To-Do:
+# - Support for backporting a PR before it is merged
+# - Automatically backport all PRs in the "Waiting to be backported" column using a command like:
+# $ curl -s -H "Authorization: token ${GITHUB_TOKEN}" -H "Accept: application/vnd.github.inertia-preview+json" https://api.github.com/projects/columns/1358120/cards | jq -r '.[].content_url' | grep issue | sed 's/^.*issues\/\([0-9]*\)$/\1/' | tac
+# (The ID of the column must first be obtained through https://api.github.com/repos/coq/coq/projects then https://api.github.com/projects/819866/columns.)
+# - Then move each of the backported PR to the subsequent columns automatically as well...
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
new file mode 100755
index 0000000000..f770004a5c
--- /dev/null
+++ b/dev/tools/merge-pr.sh
@@ -0,0 +1,48 @@
+#!/bin/sh -e
+
+# This script depends (at least) on git and jq.
+# It should be used like this: dev/tools/merge-pr.sh /PR number/
+
+#TODO: check arguments and show usage if relevant
+
+PR=$1
+
+CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD`
+REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote`
+git fetch $REMOTE refs/pull/$PR/head
+
+API=https://api.github.com/repos/coq/coq
+
+BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'`
+
+COMMIT=`git rev-parse $REMOTE/pr/$PR`
+STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'`
+
+if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+  echo "Wrong base branch"
+  read -p "Bypass? [y/n] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+fi;
+
+if [ $STATUS != "success" ]; then
+  echo "CI status is \"$STATUS\""
+  read -p "Bypass? [y/n] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+fi;
+
+git merge -S --no-ff $REMOTE/pr/$PR -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
+
+# TODO: improve this check
+if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then
+  echo "******************************************"
+  echo "** WARNING: does this PR have overlays? **"
+  echo "******************************************"
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4e7b94e419..832040ad2c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -18,7 +18,6 @@ open Univ
 open Environ
 open Printer
 open Constr
-open Evd
 open Goptions
 open Genarg
 open Clenv
@@ -62,7 +61,7 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 (* term printers *)
 let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
 let rawdebug = ref false
-let ppevar evk = pp (str (Evd.string_of_existential evk))
+let ppevar evk = pp (Evar.print evk)
 let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
 let ppeconstr x = pp (Termops.print_constr x)
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
@@ -263,7 +262,7 @@ let constr_display csr =
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
-  | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
+  | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")"
   | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
   | Ind ((sp,i),u) ->
       "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"