4 files changed, 60 insertions, 3 deletions
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/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/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
index 190511d957..d85d651070 100755
--- a/dev/tools/should-check-whitespace.sh
+++ b/dev/tools/should-check-whitespace.sh
@@ -2,4 +2,5 @@
 
 # determine if a file has whitespace checking enabled in .gitattributes
 
+git ls-files --error-unmatch "$1" >/dev/null 2>&1 &&
 git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$'
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)^")"