9 files changed, 261 insertions, 36 deletions
diff --git a/dev/base_include b/dev/base_include
index 3320a2a942..e76044f415 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -230,9 +230,9 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
+  (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
 
 let _ =
  print_string
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index bea30b1a72..8e0d2341d0 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -854,7 +854,7 @@ function make_ocaml_libs {
 
 function make_findlib {
   make_ocaml
-  if build_prep http://download.camlcity.org/download findlib-1.5.6 tar.gz 1 ; then
+  if build_prep https://opam.ocaml.org/archives ocamlfind.1.5.6+opam tar.gz 1 ; then
     logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
     # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
     log2 make all
@@ -1334,9 +1334,8 @@ function make_coq_installer {
 }
 
 ###################### ADDONS #####################
-
 function make_addon_bignums {
-  if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then
+  if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1; then
     # To make command lines shorter :-(
     echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
     logn make make all
diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
new file mode 100644
index 0000000000..df3e9cef28
--- /dev/null
+++ b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then
+
+    ltac2_CI_BRANCH=located+vernac_2
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=located+vernac_2
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    # fiat_parsers_CI_BRANCH=located+vernac
+    # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+    Elpi_CI_BRANCH=located+vernac_2
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+fi
diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
new file mode 100644
index 0000000000..a785290e7c
--- /dev/null
+++ b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then
+
+    ltac2_CI_BRANCH=located+libnames
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=located+libnames
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    Elpi_CI_BRANCH=located+libnames
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+    coq_dpdgraph_CI_BRANCH=located+libnames
+    coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git
+
+fi
diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
new file mode 100644
index 0000000000..5dedca0ca5
--- /dev/null
+++ b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then
+
+    Equations_CI_BRANCH=ssr+correct_packing
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    ltac2_CI_BRANCH=ssr+correct_packing
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Elpi_CI_BRANCH=ssr+correct_packing
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
new file mode 100644
index 0000000000..71fc396088
--- /dev/null
+++ b/dev/doc/MERGING.md
@@ -0,0 +1,78 @@
+# Merging changes in Coq
+
+This document describes how patches (submitted as Pull Requests) should be
+merged into the main repository (https://github.com/coq/coq).
+
+## Code owners
+
+The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
+system, two owners. One is the principal maintainer of the component, the other
+is the secondary maintainer.
+
+When a pull request is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the pull request touches several parts, all the
+corresponding principal maintainers will be asked for a review.
+
+Maintainers are never assigned as reviewer on their own PRs.
+
+If a principal maintainer submits a PR that changes the component they own, they
+must assign the secondary maintainer as reviewer. They should also do it if they
+know they are not available to do the review.
+
+## Reviewing
+
+When maintainers receive a review request, they are expected to:
+
+* Put their name in the assignee field, if they are in charge of the component
+  that is the main target of the patch (or if they are the only maintainer asked
+  to review the PR).
+* Review the PR, approve it or request changes.
+* If they are the assignee, check if all reviewers approved the PR. If not,
+  regularly ping the author (if changes should be implemented) or the reviewers
+  (if reviews are missing). The assignee ensures that any requests for more
+  discussion have been granted. When the discussion has converged and ALL
+  REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
+  process described below.
+
+In all cases, maintainers can delegate reviews to the other maintainer of the
+same component, except if it would lead to a maintainer reviewing their own
+patch.
+
+A maintainer is expected to be reasonably reactive, but no specific timeframe is
+given for reviewing.
+
+(*) In case a component is touched in a trivial way (adding/removing one file in
+a `Makefile`, etc), or by applying a systematic process (global renaming,
+deprecationg propagation, etc) that has been reviewed globally, the assignee can
+say in a comment they think a review is not required and proceed with the merge.
+
+## Merging
+
+Once all reviewers approved the PR, the assignee is expected to check that CI
+completed without relevant failures, and that the PR comes with appropriate
+documentation and test cases. If not, they should leave a comment on the PR and
+put the approriate label. Otherwise, they are expected to merge the PR using the
+[merge script](/dev/tools/merge-pr.sh).
+
+When the PR has conflicts, the assignee can either:
+- ask the author to rebase the branch, fixing the conflicts
+- warn the author that they are going to rebase the branch, and push to the
+  branch directly
+
+In both cases, CI should be run again.
+
+In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+the conflicts in the merge commit (following the same steps as below), and push
+to `master` directly. Don't use the GitHub interface to fix these conflicts.
+
+The command to be used is:
+```
+$ dev/tools/merge-pr XXXX
+```
+where `XXXX` is the number of the PR to be merged. This operation should be followed by a push.
+
+Maintainers MUST NOT merge their own patches.
+
+DON'T USE the GitHub interface for merging, since it will prevent the automated
+backport script from operating properly, generates bad commit messages, and a
+messy history when there are conflicts.
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 9f24960fff..2f6f1af541 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -1,50 +1,157 @@
 #!/usr/bin/env bash
 
 set -e
+set -o pipefail
+
+API=https://api.github.com/repos/coq/coq
+OFFICIAL_REMOTE_URL="git@github.com:coq/coq"
 
 # 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
+RED="\033[31m"
+RESET="\033[0m"
+GREEN="\033[32m"
+BLUE="\033[34m"
+YELLOW="\033[33m"
+info() {
+  echo -e "${GREEN}info:${RESET} $1 ${RESET}"
+}
+error() {
+  echo -e "${RED}error:${RESET} $1 ${RESET}"
+}
+warning() {
+  echo -e "${YELLOW}warning:${RESET} $1 ${RESET}"
+}
 
-PR=$1
+check_util() {
+if ! command -v "$1" > /dev/null 2>&1; then
+  error "this script requires the $1 command line utility"
+  exit 1
+fi
+}
 
-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"
+ask_confirmation() {
+  read -p "Continue anyway? [y/N] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+}
 
-API=https://api.github.com/repos/coq/coq
+check_util jq
+check_util curl
+check_util git
+check_util gpg
+
+# command line parsing
+
+if [ $# != 1 ]; then
+  error "usage: $0 PR-number"
+  exit 1
+fi
+
+if [[ "$1" =~ ^[1-9][0-9]*$ ]]; then
+  PR=$1
+else
+  error "$1 is not a number"
+  exit 1
+fi
+
+# Fetching PR metadata
+
+TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title')
+info "title for PR $PR is ${BLUE}$TITLE"
 
 BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+info "PR $PR targets branch ${BLUE}$BASE_BRANCH"
+
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH"
 
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+if [ -z "$REMOTE" ]; then
+  error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote"
+  error "don't know where to fetch the PR from"
+  error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
+  exit 1
+fi
+REMOTE_URL=$(git remote get-url "$REMOTE" --push)
+if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \
+     "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
+  error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
+  error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
+  error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
+  ask_confirmation
+fi
+info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE"
+
+info "fetching from $REMOTE the PR"
+git remote update "$REMOTE"
+if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then
+  error "remote $REMOTE is not configured to fetch pull requests"
+  error "run: git config remote.$REMOTE.fetch +refs/pull/*/head:refs/remotes/$REMOTE/pr/*"
+  exit 1
+fi
+git fetch "$REMOTE" "refs/pull/$PR/head"
 COMMIT=$(git rev-parse FETCH_HEAD)
-STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+info "commit for PR $PR is ${BLUE}$COMMIT"
+
+# Sanity check: merge to a different branch
 
 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
+  error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH"
+  ask_confirmation
 fi;
 
+# Sanity check: CI failed
+
+STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+
 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
+  error "CI unsuccessful on ${BLUE}$(curl -s "$API/commits/$COMMIT/status" |
+    jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')"
+  ask_confirmation
 fi;
 
-git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
+# Sanity check: has labels named "needs:"
+
+NEEDS_LABELS=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
+if [ "$NEEDS_LABELS" != "[]" ]; then
+  error "needs:something labels still present: ${BLUE}$NEEDS_LABELS"
+  ask_confirmation
+fi
+
+# Sanity check: has milestone
+
+MILESTONE=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title')
+if [ "$MILESTONE" = "null" ]; then
+  error "no milestone set, please set one"
+  ask_confirmation
+fi
+
+# Sanity check: has kind
+
+KIND=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
+if [ "$KIND" = "[]" ]; then
+  error "no kind:something label set, please set one"
+  ask_confirmation
+fi
+
+# Sanity check: user.signingkey
+if [ -z "$(git config user.signingkey)" ]; then
+  warning "git config user.signingkey is empty"
+  warning "gpg will guess a key out of your git config user.* data"
+fi
+
+info "merging"
+git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e
 
 # TODO: improve this check
-if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
-  echo "******************************************"
-  echo "** WARNING: does this PR have overlays? **"
-  echo "******************************************"
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then
+  warning "this PR may have overlays (sorry the check is not perfect)"
+  warning "if it has overlays please check the following:"
+  warning "- each overlay has a corresponding open PR on the upstream repo"
+  warning "- after merging please notify the upstream they can merge the PR"
 fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 74cdd788b4..ba0c54407c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -547,7 +547,7 @@ let encode_path ?loc prefix mpdir suffix id =
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
-  Qualid (Loc.tag ?loc @@ make_qualid
+  CAst.make ?loc @@ Qualid (make_qualid
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
 let raw_string_of_ref ?loc _ = function
@@ -567,9 +567,9 @@ let raw_string_of_ref ?loc _ = function
       encode_path ?loc "SECVAR" None [] id
 
 let short_string_of_ref ?loc _ = function
-  | VarRef id -> Ident (Loc.tag ?loc id)
-  | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn)))
+  | VarRef id -> CAst.make ?loc @@ Ident id
+  | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn)))
   | IndRef (kn,i) ->
       encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
         (Id.of_string ("_"^string_of_int i))
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index e47be638aa..dad6dcc1c0 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -153,7 +153,7 @@ val ppnamedcontextval : Environ.named_context_val -> unit
 val ppenv : Environ.env -> unit
 val ppenvwithcst : Environ.env -> unit
 
-val pptac : Tacexpr.glob_tactic_expr -> unit
+val pptac : Ltac_plugin.Tacexpr.glob_tactic_expr -> unit
 
 val ppobj : Libobject.obj -> unit