Merge remote-tracking branch 'origin/master' into stm+doc_hook

26 files changed, 100 insertions, 89 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 4c5bd29236..d737632638 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1316,7 +1316,6 @@ function copy_coq_license {
     # FIXME: this is not the micromega license
     # It only applies to code that was copied into one single file!
     install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
@@ -1631,19 +1630,6 @@ function make_addon_ssreflect {
   fi
 }
 
-# Ltac-2 plugin
-# A new (experimental) tactic language
-
-function make_addon_ltac2 {
-  installer_addon_dependency ltac2
-  if build_prep_overlay ltac2; then
-    installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
-    log1 make $MAKE_OPT all
-    log2 make install
-    build_post
-  fi
-}
-
 # UniCoq plugin
 # An alternative unification algorithm
 function make_addon_unicoq {
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
deleted file mode 100644
index f26e0904bc..0000000000
--- a/dev/ci/appveyor.sh
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/bash
-
-set -e -x
-
-APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c
-NJOBS=2
-
-wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
-tar -xf opam64.tar.xz
-bash opam64/install.sh
-
-opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing
-eval "$(opam env)"
-opam install -j $NJOBS -y num ocamlfind ounit
-
-# Full regular Coq Build
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4f5988c59c..95fceb773a 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -81,13 +81,6 @@
 : "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}"
 
 ########################################################################
-# Ltac2
-########################################################################
-: "${ltac2_CI_REF:=master}"
-: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}"
-: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}"
-
-########################################################################
 # GeoCoq
 ########################################################################
 : "${GeoCoq_CI_REF:=master}"
@@ -105,7 +98,8 @@
 # Coquelicot
 ########################################################################
 : "${coquelicot_CI_REF:=master}"
-: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
 
 ########################################################################
 # CompCert
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 33627fd8ef..6cb8dad604 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
 
 install_ssreflect
 
-FORCE_GIT=1
 git_download coquelicot
 
 ( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
deleted file mode 100755
index 4df22bf249..0000000000
--- a/dev/ci/ci-ltac2.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download ltac2
-
-( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install )
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index cc1931d13d..6c4ccfc14d 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -41,7 +41,6 @@ IF "%WINDOWS%" == "enabled_all_addons" (
   SET EXTRA_ADDONS=^

     -addon=bignums ^

     -addon=equations ^

-    -addon=ltac2 ^

     -addon=mtac2 ^

     -addon=mathcomp ^

     -addon=menhir ^

diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
index 1d931c858e..d813ddd8d7 100644
--- a/dev/ci/nix/bignums.nix
+++ b/dev/ci/nix/bignums.nix
@@ -1,5 +1,5 @@
 { ocamlPackages }:
 
 {
-  buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+  buildInputs = [ ocamlPackages.ocaml ];
 }
diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix
new file mode 100644
index 0000000000..d379bfa73d
--- /dev/null
+++ b/dev/ci/nix/coquelicot.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ssreflect }:
+
+{
+  buildInputs = [ autoconf automake ];
+  coqBuildInputs = [ ssreflect ];
+  configure = "./autogen.sh && ./configure";
+  make = "./remake";
+  clean = "./remake clean";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 17070e66ee..a9cc91170f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -72,6 +72,7 @@ let projects = {
   CoLoR = callPackage ./CoLoR.nix {};
   CompCert = callPackage ./CompCert.nix {};
   coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+  coquelicot = callPackage ./coquelicot.nix {};
   Corn = callPackage ./Corn.nix {};
   cross_crypto = callPackage ./cross_crypto.nix {};
   Elpi = callPackage ./Elpi.nix {};
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
index e153043557..71028ec2dc 100644
--- a/dev/ci/nix/flocq.nix
+++ b/dev/ci/nix/flocq.nix
@@ -4,4 +4,5 @@
   buildInputs = [ autoconf automake ];
   configure = "./autogen.sh && ./configure";
   make = "./remake";
+  clean = "./remake clean";
 }
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
index 6d96d94dfc..6d2f6470b1 100644
--- a/dev/ci/nix/unicoq/unicoq-num.patch
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -4,19 +4,6 @@ Date:   Thu Nov 29 08:59:22 2018 +0000
 
     Make explicit dependency to num
 
-diff --git a/Make b/Make
-index 550dc6a..8aa1309 100644
---- a/Make
-+++ b/Make
-@@ -9,7 +9,7 @@ src/logger.ml
- src/munify.mli
- src/munify.ml
- src/unitactics.mlg
--src/unicoq.mllib
-+src/unicoq.mlpack
- theories/Unicoq.v
- test-suite/munifytest.v
- test-suite/microtests.v
 diff --git a/Makefile.local b/Makefile.local
 new file mode 100644
 index 0000000..88be365
@@ -24,21 +11,3 @@ index 0000000..88be365
 +++ b/Makefile.local
 @@ -0,0 +1 @@
 +CAMLPKGS += -package num
-diff --git a/src/unicoq.mllib b/src/unicoq.mllib
-deleted file mode 100644
-index 2b84e2d..0000000
---- a/src/unicoq.mllib
-+++ /dev/null
-@@ -1,3 +0,0 @@
--Logger
--Munify
--Unitactics
-diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
-new file mode 100644
-index 0000000..2b84e2d
---- /dev/null
-+++ b/src/unicoq.mlpack
-@@ -0,0 +1,3 @@
-+Logger
-+Munify
-+Unitactics
diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
new file mode 100644
index 0000000000..dc39ea5ef0
--- /dev/null
+++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then
+
+    equations_CI_BRANCH=master+fix-evars_of_term-pr8893
+    equations_CI_REF=master+fix-evars_of_term-pr8893
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
new file mode 100644
index 0000000000..9f9cc19e83
--- /dev/null
+++ b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then
+
+    relation_algebra_CI_REF=cleanup-logic-convert-hyp
+    relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra
+
+fi
diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
new file mode 100644
index 0000000000..0e1449f36c
--- /dev/null
+++ b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then
+
+    unicoq_CI_REF=whd-for-evar-conv-no-stack
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+    elpi_CI_REF=canonical-disable-hint
+    elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
new file mode 100644
index 0000000000..4032b1c6b5
--- /dev/null
+++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then
+
+    paramcoq_CI_REF=run_tactic_gen
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
new file mode 100644
index 0000000000..bc8aa33565
--- /dev/null
+++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then
+
+    unicoq_CI_REF=detype-anonymous
+    unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh
new file mode 100644
index 0000000000..fcbeb32a58
--- /dev/null
+++ b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10188" ] || [ "$CI_BRANCH" = "def-not-visible-remove-warning" ]; then
+
+    elpi_CI_REF=def-not-visible-generic-warning
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 3f1b470878..c9eceb1270 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -71,8 +71,9 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or
-the [`dev/doc/changes.md`](changes.md) file.
+Moreover the PR author *must* add an entry to the [unreleased
+changelog](../../doc/changelog/README.md) or to the
+[`dev/doc/changes.md`](changes.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9e0d47651e..7221c3de56 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,10 @@
+## Changes between Coq 8.10 and Coq 8.11
+
+### ML API
+
+- Functions and types deprecated in 8.10 have been removed in Coq
+  8.11.
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 60c0886896..189d6f9fa5 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -84,10 +84,18 @@
   Coq has been tagged.
 - [ ] Have some people test the recently auto-generated Windows and MacOS
   packages.
-- [ ] Change the version name from alpha to beta1 (see
+- [ ] In a PR:
+  - Change the version name from alpha to beta1 (see
   [#7009](https://github.com/coq/coq/pull/7009/files)).
-  We generally do not update the magic numbers at this point.
+  - We generally do not update the magic numbers at this point.
+  - Set `is_a_released_version` to `true` in `configure.ml`.
 - [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+- [ ] Check using `git push --tags --dry-run` that you are not
+  pushing anything else than the new tag. If needed, remove spurious
+  tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+  (if you forget about it, you'll be reminded whenever you try to
+  backport a PR with a changelog entry).
 
 ### These steps are the same for all releases (beta, final, patch-level) ###
 
@@ -112,9 +120,17 @@
 
 ## At the final release time ##
 
-- [ ] Change the version name to X.X.0 and the magic numbers (see
+- [ ] In a PR:
+  - Change the version name from X.X.0 and the magic numbers (see
   [#7271](https://github.com/coq/coq/pull/7271/files)).
+  - Set `is_a_released_version` to `true` in `configure.ml`.
 - [ ] Put the `VX.X.0` tag.
+- [ ] Check using `git push --tags --dry-run` that you are not
+  pushing anything else than the new tag. If needed, remove spurious
+  tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+  (if you forget about it, you'll be reminded whenever you try to
+  backport a PR with a changelog entry).
 
 Repeat the generic process documented above for all releases.
 
diff --git a/dev/include_printers b/dev/include_printers
index 90088e40bf..d077075eeb 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -11,6 +11,7 @@
 #install_printer  (* universes *)  ppuniverses;;
 #install_printer  (* univ level *) ppuni_level;;
 #install_printer  (* univ context *) ppuniverse_context;;
+#install_printer  (* univ context *) ppaucontext;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
 #install_printer  (* univ set *) ppuniverse_set;;
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index f4786d9431..8dfe1e7833 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/8471ab76242987b11afd4486b82888e1588f8307.tar.gz";
-  sha256 = "06pp6b6x78jlinxifnphkbp79dx58jr990fkm4qziq0ay5klpxd7";
+  url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz";
+  sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1";
 })
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index a6ecec7e33..82f2e79549 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level
 install_printer Top_printers.ppuniverse_set
 install_printer Top_printers.ppuniverse_instance
 install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppaucontext
 install_printer Top_printers.ppuniverse_context_set
 install_printer Top_printers.ppuniverse_subst
 install_printer Top_printers.ppuniverse_opt_subst
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 816316487c..2859b56cbe 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,7 +27,6 @@ open Clenv
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
 
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
@@ -236,6 +235,15 @@ let ppnamedcontextval e =
   let sigma = Evd.from_env env in
   pp (pr_named_context env sigma (named_context_of_val e))
 
+let ppaucontext auctx =
+  let nas = AUContext.names auctx in
+  let prlev l = match Level.var_index l with
+    | Some n -> Name.print nas.(n)
+    | None -> prlev l
+  in
+  pp (pr_universe_context prlev (AUContext.repr auctx))
+
+
 let ppenv e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index cb32d2294c..2aa1808322 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
 val ppuniverse_set : Univ.LSet.t -> unit
 val ppuniverse_instance : Univ.Instance.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
+val ppaucontext : Univ.AUContext.t -> unit
 val ppuniverse_context_set : Univ.ContextSet.t -> unit
 val ppuniverse_subst : Univ.universe_subst -> unit
 val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit