9 files changed, 97 insertions, 45 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 95fceb773a..fa39b41565 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -215,7 +215,7 @@
 ########################################################################
 # simple-io
 ########################################################################
-: "${simple_io_CI_REF:=dev}"
+: "${simple_io_CI_REF:=master}"
 : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}"
 : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}"
 
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index bba17314f7..e8c8d22678 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -11,7 +11,7 @@ git_download fiat_crypto
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
 
 fiat_crypto_CI_TARGETS1="c-files printlite lite"
-fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem"
+fiat_crypto_CI_TARGETS2="coq"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
         ulimit -s 32768 && \
diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh
new file mode 100644
index 0000000000..242b177d71
--- /dev/null
+++ b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh
@@ -0,0 +1,23 @@
+if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then
+
+    fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726
+    fiat_parsers_CI_REF=master+change-for-coq-pr8726
+    fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat
+
+    elpi_CI_BRANCH=coq-master+fix-global-pr8726
+    elpi_CI_REF=coq-master+fix-global-pr8726
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+    equations_CI_BRANCH=master+fix-global-pr8726
+    equations_CI_REF=master+fix-global-pr8726
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+    mtac2_CI_BRANCH=master+fix-global-pr8726
+    mtac2_CI_REF=master+fix-global-pr8726
+    mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+    paramcoq_CI_BRANCH=master+fix-global-pr8726
+    paramcoq_CI_REF=master+fix-global-pr8726
+    paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh
new file mode 100644
index 0000000000..e4cf74aa51
--- /dev/null
+++ b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9566" ] || [ "$CI_BRANCH" = "proof_global+move_termination_routine_out" ]; then
+
+    aac_tactics_CI_REF=proof_global+move_termination_routine_out
+    aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+    equations_CI_REF=proof_global+move_termination_routine_out
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    paramcoq_CI_REF=proof_global+move_termination_routine_out
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh
new file mode 100644
index 0000000000..2c3f490c03
--- /dev/null
+++ b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then
+
+    equations_CI_REF=rm-kernel-sideeff-role
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 339ac2d9b7..51d90df89f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,6 +5,21 @@
 - Functions and types deprecated in 8.10 have been removed in Coq
   8.11.
 
+- Type Decl_kinds.locality has been restructured, see commit
+  message. Main change to do generally is to change the flag "Global"
+  to "Global ImportDefaultBehavior".
+
+Proof state:
+
+  Proofs that are attached to a top-level constant (such as lemmas)
+  are represented by `Lemmas.t`, as they do contain additional
+  information related to the constant declaration.
+
+  Plugins that require access to the information about currently
+  opened lemmas can add one of the `![proof]` attributes to their
+  `mlg` entry, which will refine the type accordingly. See
+  documentation in `vernacentries` for more information.
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing
@@ -59,6 +74,19 @@ Coqlib:
   command then enables to locate the registered constant through its name. The
   name resolution is dynamic.
 
+Proof state:
+
+- Handling of proof state has been fully functionalized, thus it is
+  not possible to call global functions such as `get_current_context ()`.
+
+  The main type for functions that need to handle proof state is
+  `Proof_global.t`.
+
+  Unfortunately, this change was not possible to do in a
+  backwards-compatible way, but in most case the api changes are
+  straightforward, with functions taking and returning an extra
+  argument.
+
 Macros:
 
 - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
index 96c92e3162..539bb5f1f9 100755
--- a/dev/lint-commits.sh
+++ b/dev/lint-commits.sh
@@ -19,21 +19,40 @@ fi
 BASE_COMMIT="$1"
 HEAD_COMMIT="$2"
 
-bad=()
+bad_ws=()
+bad_compile=()
 while IFS= read -r commit; do
     echo Checking "$commit"
     # git diff --check
     # uses .gitattributes to know what to check
     if ! git diff --check "${commit}^" "$commit";
-    then
-        bad+=("$commit")
+    then bad_ws+=("$commit")
+    fi
+
+    if ! make -f Makefile.dune check
+    then bad_compile+=("$commit")
     fi
 done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --)
 
-if [ "${#bad[@]}" != 0 ]
+# report errors
+
+CODE=0
+
+if [ "${#bad_ws[@]}" != 0 ]
 then
     >&2 echo "Whitespace errors!"
-    >&2 echo "In commits ${bad[*]}"
+    >&2 echo "In commits ${bad_ws[*]}"
     >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
-    exit 1
+    >&2 echo
+    CODE=1
 fi
+
+if [ "${#bad_compile[@]}" != 0 ]
+then
+    >&2 echo "Compilation errors!"
+    >&2 echo "In commits ${bad_compile[*]}"
+    >&2 echo
+    CODE=1
+fi
+
+exit $CODE
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index b89ae67a82..5f9f326750 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -78,11 +78,7 @@ Specifically `camldebug-command-name' and `ocamldebug-command-name'."
 Note that this function is executed before _Coqproject is read if it exists."
   (let ((dir (coqdev-default-directory)))
     (when dir
-      (unless coq-prog-args
-        (setq coq-prog-args
-              `("-coqlib" ,dir
-                "-topfile" ,buffer-file-name)))
-      (setq-local coq-prog-name (concat dir "bin/coqtop")))))
+      (setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude")))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
 
 (defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg"
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index ff9b32fe78..0338cd42c7 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -73,8 +73,6 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
 COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
 G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
-BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
-BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
                          for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
@@ -401,34 +399,6 @@ dev/tools/update-compat.py --assert-unchanged %s || exit $?
 ''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip()
     update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args)
 
-def update_bug_4789(new_versions, **args):
-    # we always update this compat notation to oldest
-    # currently-supported compat version, which should never be the
-    # current version
-    with open(BUG_4798_PATH, 'r') as f: contents = f.read()
-    new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "%s").
-Check match 2 with 0 => 0 | S n => n end. (* fails *)
-""" % new_versions[0]
-    update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
-
-def update_bug_9166(new_versions, **args):
-    # we always update this compat notation to oldest
-    # currently-supported compat version, which should never be the
-    # current version
-    with open(BUG_9166_PATH, 'r') as f: contents = f.read()
-    new_contents = BUG_HEADER + r"""Set Warnings "+deprecated".
-
-Notation bar := option (compat "%s").
-
-Definition foo (x: nat) : nat :=
-  match x with
-  | 0 => 0
-  | S bar => bar
-  end.
-""" % new_versions[0]
-    update_if_changed(contents, new_contents, BUG_9166_PATH, **args)
-
 def update_compat_notations_in(old_versions, new_versions, contents):
     for v in old_versions:
         if v not in new_versions:
@@ -508,7 +478,5 @@ if __name__ == '__main__':
     update_test_suite(new_versions, **args)
     update_test_suite_run(**args)
     update_doc_index(new_versions, **args)
-    update_bug_4789(new_versions, **args)
-    update_bug_9166(new_versions, **args)
     update_compat_notations(known_versions, new_versions, **args)
     display_git_grep(known_versions, new_versions)