10 files changed, 67 insertions, 20 deletions
diff --git a/dev/base_include b/dev/base_include
index 574bc097e..6f54ecb24 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -229,7 +229,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
+  (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);;
 
 let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 665b3768a..08364c897 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -47,16 +47,13 @@ CI.
 
 ### Add your development by submitting a pull request
 
-Add a new `ci-mydev.sh` script to [`dev/ci`](.) (have a look at
-[`ci-coq-dpdgraph.sh`](ci-coq-dpdgraph.sh) or
-[`ci-fiat-parsers.sh`](ci-fiat-parsers.sh) for simple examples);
-set the corresponding variables in
-[`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the corresponding
-target to [`Makefile.ci`](../../Makefile.ci); add new jobs to
-[`.gitlab-ci.yml`](../../.gitlab-ci.yml),
-[`.circleci/config.yml`](../../.circleci/config.yml) and
-[`.travis.yml`](../../.travis.yml) so that this new target is run. **Do not
-hesitate to submit an incomplete pull request if you need help to finish it.**
+Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
+variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the
+corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to
+[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run.
+Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an
+example. **Do not hesitate to submit an incomplete pull request if you need
+help to finish it.**
 
 You may also be interested in having your development tested in our
 performance benchmark. Currently this is done by providing an OPAM package
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 87d837b38..3807ff90c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -119,7 +119,7 @@
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}"
+: "${coq_dpdgraph_CI_BRANCH:=coq-master}"
 : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}"
 
 ########################################################################
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 1a83593f5..52f851917 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-06-04-V2"
+# CACHEKEY: "bionic_coq-V2018-06-13-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -27,7 +27,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 jbuilder.1.0+beta20 ounit.2.0.8" \
-    CI_OPAM="menhir.20180530 elpi.1.0.3 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV CAMLP5_VER="6.14" \
diff --git a/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh b/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh
new file mode 100644
index 000000000..9d96b6d4c
--- /dev/null
+++ b/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh
@@ -0,0 +1,4 @@
+ if [ "$CI_PULL_REQUEST" = "664" ] || [ "$CI_BRANCH" = "trunk+fix-5500-too-weak-test-return-clause" ]; then
+    fiat_parsers_CI_BRANCH=master+change-for-coq-pr664-compatibility
+    fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat
+fi
diff --git a/dev/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh
new file mode 100644
index 000000000..f7811cd6f
--- /dev/null
+++ b/dev/ci/user-overlays/07797-rm-reference.sh
@@ -0,0 +1,20 @@
+_OVERLAY_BRANCH=rm-reference
+
+if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git
+
+    ltac2_CI_BRANCH="fix-7797"
+    ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git
+
+    quickchick_CI_BRANCH="$_OVERLAY_BRANCH"
+    quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git
+
+    coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH"
+    coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git
+
+    Elpi_CI_BRANCH="$_OVERLAY_BRANCH"
+    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index bb8189efc..f3fc126f9 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,14 @@
 
 ### ML API
 
+Names
+
+- In `Libnames`, the type `reference` and its two constructors `Qualid` and
+  `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
+  `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
+  replaced by a test using `qualid_is_ident`. Extracting the ident part of a
+  qualid can be done using `qualid_basename`.
+
 Misctypes
 
 - Syntax for universe sorts and kinds has been moved from `Misctypes`
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 9d2ebf0d4..b5dd8445d 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
 
 In Coq source folder:
 
-opam switch 4.02.1+fp
+opam switch 4.02.3+fp
 ./configure -local -debug
 make
 perf record -g bin/coqtop -compile file.v
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 00d04e6b3..320ef6ed0 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -140,6 +140,24 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
     fi
 fi
 
+# Sanity check: PR has an outdated version of CI
+
+BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
+CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml")
+
+if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
+then
+    warning "This PR didn't run with the latest version of CI."
+    warning "It is probably a good idea to ask for a rebase."
+    read -p "Do you want to see the diff? [Y/n] " $QUICK_CONF -r
+    echo
+    if [[ ! $REPLY =~ ^[Nn]$ ]]
+    then
+        git diff "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
+    fi
+    ask_confirmation
+fi
+
 # Sanity check: CI failed
 
 STATUS=$(curl -s "$API/commits/$COMMIT/status")
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 10a7a4158..844ad9188 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id =
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
-  CAst.make ?loc @@ Qualid (make_qualid
-    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
+  make_qualid ?loc
+    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
@@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function
       encode_path ?loc "SECVAR" None [] id
 
 let short_string_of_ref ?loc _ = function
-  | 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)))
+  | VarRef id -> qualid_of_ident ?loc id
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (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))