6 files changed, 59 insertions, 16 deletions
diff --git a/dev/base_include b/dev/base_include
index 574bc097e5..6f54ecb241 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 665b3768a4..08364c897a 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/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh
new file mode 100644
index 0000000000..f7811cd6f8
--- /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 bb8189efc7..f3fc126f92 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/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 00d04e6b3d..320ef6ed07 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 10a7a4158b..844ad9188a 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))