12 files changed, 56 insertions, 200 deletions
diff --git a/dev/ci/ci-argosy.sh b/dev/ci/ci-argosy.sh
new file mode 100755
index 0000000000..6137526bf4
--- /dev/null
+++ b/dev/ci/ci-argosy.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+FORCE_GIT=1
+git_download argosy
+
+( cd "${CI_BUILD_DIR}/argosy" && git submodule update --init --recursive && make )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 62335ea5d0..0c89809ee9 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -104,15 +104,8 @@
 ########################################################################
 # Coquelicot
 ########################################################################
-# The URL for downloading a tgz snapshot of the master branch is
-# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz
-# See https://gforge.inria.fr/scm/browser.php?group_id=3599
-# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently,
-# we use a fixed version, which has a download path which does fit to our standard mechanism.
-# ATTENTION: The archive URL might depend on the version!
-: "${Coquelicot_CI_REF:=coquelicot-3.0.2}"
-: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
-: "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}"
+: "${coquelicot_CI_REF:=master}"
+: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
 
 ########################################################################
 # CompCert
@@ -296,3 +289,10 @@
 : "${stdlib2_CI_REF:=master}"
 : "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}"
 : "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}"
+
+########################################################################
+# argosy
+########################################################################
+: "${argosy_CI_REF:=master}"
+: "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}"
+: "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2d242d80a4..2ac78d3c2b 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 5d8817491d..33627fd8ef 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -6,6 +6,6 @@ ci_dir="$(dirname "$0")"
 install_ssreflect
 
 FORCE_GIT=1
-git_download Coquelicot
+git_download coquelicot
 
-( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 5f819f31f9..cc1931d13d 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -49,9 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
     -addon=compcert ^
     -addon=extlib ^
     -addon=quickchick ^
-    -addon=coquelicot ^
     -addon=vst ^
     -addon=aactactics
+REM -addon=coquelicot ^
 ) ELSE (
   SET "EXTRA_ADDONS= "
 )
diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh
new file mode 100644
index 0000000000..c04621114f
--- /dev/null
+++ b/dev/ci/user-overlays/08829-proj-syntax-check.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then
+    lambdaRust_CI_REF=proj-syntax-check
+    lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust
+    lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive
+fi
diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
new file mode 100644
index 0000000000..12be1b676a
--- /dev/null
+++ b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then
+
+    HoTT_CI_REF=rm-hardwired-hint-db
+    HoTT_CI_GITURL=https://github.com/vbgl/HoTT
+
+    ltac2_CI_REF=rm-hardwired-hint-db
+    ltac2_CI_GITURL=https://github.com/vbgl/ltac2
+
+    UniMath_CI_REF=rm-hardwired-hint-db
+    UniMath_CI_GITURL=https://github.com/vbgl/UniMath
+
+fi
diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh
new file mode 100644
index 0000000000..b17454fc4c
--- /dev/null
+++ b/dev/ci/user-overlays/09733-gares-quotations.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then
+
+    ltac2_CI_REF=quotations
+    ltac2_CI_GITURL=https://github.com/gares/ltac2
+
+fi
diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh
new file mode 100644
index 0000000000..4b49011de3
--- /dev/null
+++ b/dev/ci/user-overlays/09815-token-type.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then
+    ltac2_CI_REF=token-type
+    ltac2_CI_GITURL=https://github.com/proux01/ltac2
+fi
diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh
new file mode 100644
index 0000000000..bb14a8c204
--- /dev/null
+++ b/dev/ci/user-overlays/09870-vbgl-recordops.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then
+
+    elpi_CI_REF=pr-9870
+    elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/dev/doc/archive/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY
index a81afca32d..35a7f608de 100644
--- a/dev/doc/archive/COMPATIBILITY
+++ b/dev/doc/archive/COMPATIBILITY
@@ -1,192 +1,6 @@
 Note: this file isn't used anymore. Incompatibilities are documented
 as part of CHANGES.
 
-Potential sources of incompatibilities between Coq V8.6 and V8.7
-----------------------------------------------------------------
-
-- Extra superfluous names in introduction patterns may now raise an
-  error rather than a warning when the superfluous name is already in
-  use. The easy fix is to remove the superfluous name.
-
-Potential sources of incompatibilities between Coq V8.5 and V8.6
-----------------------------------------------------------------
-
-Symptom: An obligation generated by Program or an abstracted subproof
-has different arguments.
-Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
-and the subproof does not use the argument.
-Remedy:
-- Adapt the script.
-- Write an explicit lemma to prove the obligation/subproof and use it
-  instead (compatible with 8.4).
-- Unset the option for the program/proof the obligation/subproof originates
-  from.
-
-Symptom: In a goal, order of hypotheses, or absence of an equality of
-the form "x = t" or "t = x", or no unfolding of a local definition.
-Cause: This might be connected to a number of fixes in the tactic
-"subst". The former behavior can be reactivated by issuing "Unset
-Regular Subst Tactic".
-  
-Potential sources of incompatibilities between Coq V8.4 and V8.5
-----------------------------------------------------------------
-
-* List of typical changes to be done to adapt files from Coq 8.4 *
-* to Coq 8.5 when not using compatibility option "-compat 8.4".  *
-
-Symptom: "The reference omega was not found in the current environment".
-Cause: "Require Omega" does not import the tactic "omega" any more
-Possible solutions:
-- use "Require Import OmegaTactic" (not compatible with 8.4)
-- use "Require Import Omega" (compatible with 8.4)
-- add definition "Ltac omega := Coq.omega.Omega.omega."
-  
-Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective)
-Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives
-Possible solutions:
-- use "dintuition" instead; it is stronger than "intuition" and works
-  uniformly on non standard connectives, such as n-ary conjunctions or disjunctions
-  (not compatible with 8.4)
-- do the script differently
-
-Symptom: The constructor foo (in type bar) expects n arguments.
-Cause: parameters must now be given in patterns
-Possible solutions:
-- use option "Set Asymmetric Patterns" (compatible with 8.4)
-- add "_" for the parameters (not compatible with 8.4)
-- turn the parameters into implicit arguments (compatible with 8.4)
-
-Symptom: "NPeano.Nat.foo" not existing anymore
-Possible solutions:
-- use "Nat.foo" instead
-
-Symptom: typing problems with proj1_sig or similar
-Cause: coercion from sig to sigT and similar coercions have been
-  removed so as to make the initial state easier to understand for
-  beginners
-Solution: change proj1_sig into projT1 and similarly (compatible with 8.4)
-
-* Other detailed changes *
-
-(see also file CHANGES)
-
-- options for *coq* compilation (see below for ocaml).
-
-** [-I foo] is now deprecated and will not add directory foo to the
-   coq load path (only for ocaml, see below). Just replace [-I foo] by
-   [-Q foo ""] in your project file and re-generate makefile. Or
-   perform the same operation directly in your makefile if you edit it
-   by hand.
-
-** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq
-   load path.
-
-** Option [-I foo -as bar] is unchanged but discouraged unless you
-   compile ocaml code. Use -Q foo bar instead.
-
-  for more details: file CHANGES or section "Customization at launch
-  time" of the reference manual.
-
-- Command line options for ocaml  Compilation of ocaml code (plugins) 
-
-** [-I foo] is *not* deprecated to add foo to the ocaml load path.
-
-** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to
-   the coq load path with logical name bar (shortcut for -I foo -Q foo
-   bar).
-
-  for more details: file CHANGES or section "Customization at launch
-  time" of the reference manual.
-
-- Universe Polymorphism.
-
-- Refinement, unification and tactics are now aware of universes,
-  resulting in more localized errors. Universe inconsistencies 
-  should no more get raised at Qed time but during the proof.
-  Unification *always* produces well-typed substitutions, hence
-  some rare cases of unifications that succeeded while producing
-  ill-typed terms before will now fail.
-  
-- The [change p with c] tactic semantics changed, now typechecking 
-  [c] at each matching occurrence [t] of the pattern [p], and 
-  converting [t] with [c].
-  
-- Template polymorphic inductive types: the partial application 
-  of a template polymorphic type (e.g. list) is not polymorphic.
-  An explicit parameter application (e.g [fun A => list A]) or
-  [apply (list _)] will result in a polymorphic instance.
-
-- The type inference algorithm now takes opacity of constants into
-  account. This may have effects on tactics using type inference
-  (e.g. induction). Extra "Transparent" might have to be added to
-  revert opacity of constants.
-
-Type classes.
-
-- When writing an Instance foo : Class A := {| proj := t |} (note the
-  vertical bars), support for typechecking the projections using the
-  type information and switching to proof mode is no longer available.
-  Use { } (without the vertical bars) instead.
-
-Tactic abstract.
-
-- Auxiliary lemmas generated by the abstract tactic are removed from
-  the global environment and inlined in the proof term when a proof
-  is ended with Qed.  The behavior of 8.4 can be obtained by ending
-  proofs with "Qed exporting" or "Qed exporting ident, .., ident".
-
-Potential sources of incompatibilities between Coq V8.3 and V8.4
-----------------------------------------------------------------
-
-(see also file CHANGES)
-
-The main known incompatibilities between 8.3 and 8.4 are consequences
-of the following changes:
-
-- The reorganization of the library of numbers:
-
-  Several definitions have new names or are defined in modules of
-  different names, but a special care has been taken to have this
-  renaming transparent for the user thanks to compatibility notations.
-
-  However some definitions have changed, what might require some
-  adaptations. The most noticeable examples are:
-  - The "?=" notation which now bind to Pos.compare rather than former
-    Pcompare (now Pos.compare_cont).
-  - Changes in names may induce different automatically generated
-    names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
-  - Z.add has a new definition, hence, applying "simpl" on subterms of
-    its body might give different results than before.
-  - BigN.shiftl and BigN.shiftr have reversed arguments order, the
-    power function in BigN now takes two BigN.
-
-- Other changes in libraries:
-
-  - The definition of functions over "vectors" (list of fixed length)
-    have changed.
-  - TheoryList.v has been removed.
-
-- Slight changes in tactics:
-
-  - Less unfolding of fixpoints when applying destruct or inversion on
-    a fixpoint hiding an inductive type (add an extra call to simpl to
-    preserve compatibility).
-  - Less unexpected local definitions when applying "destruct"
-    (incompatibilities solvable by adapting name hypotheses).
-  - Tactic "apply" might succeed more often, e.g. by now solving
-    pattern-matching of the form ?f x y = g(x,y) (compatibility
-    ensured by using "Unset Tactic Pattern Unification"), but also
-    because it supports (full) betaiota (using "simple apply" might
-    then help).
-  - Tactic autorewrite does no longer instantiate pre-existing
-    existential variables.
-  - Tactic "info" is now available only for auto, eauto and trivial.
-
-- Miscellaneous changes:
-
-  - The command "Load" is now atomic for backtracking (use "Unset
-    Atomic Load" for compatibility).
-
 
 Incompatibilities beyond 8.4...
 
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index b1bfac8cc9..49251d61a1 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -22,7 +22,7 @@ If you want to build the standard libraries and plugins you should
 call `make -f Makefile.dune voboot`. It is usually enough to do that
 once per-session.
 
-More helper targets are availabe in `Makefile.dune`, `make -f
+More helper targets are available in `Makefile.dune`, `make -f
 Makefile.dune` will display some help.
 
 Dune places build artifacts in a separate directory `_build`; it will