10 files changed, 97 insertions, 47 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index bd7ee46358..c18e556da8 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -200,6 +200,13 @@
 : "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}"
 
 ########################################################################
+# bbv
+########################################################################
+: "${bbv_CI_REF:=master}"
+: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}"
+: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}"
+
+########################################################################
 # bedrock2
 ########################################################################
 : "${bedrock2_CI_REF:=tested}"
@@ -330,3 +337,10 @@
 : "${perennial_CI_REF:=master}"
 : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
 : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+
+########################################################################
+# metacoq
+########################################################################
+: "${metacoq_CI_REF:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
+: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-bbv.sh b/dev/ci/ci-bbv.sh
new file mode 100755
index 0000000000..6892cea3e4
--- /dev/null
+++ b/dev/ci/ci-bbv.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download bbv
+
+( cd "${CI_BUILD_DIR}/bbv" && make && make install )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 871d033f5b..30047e624b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
-( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..1302065961
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download metacoq
+
+( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install )
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
new file mode 100644
index 0000000000..8a734feada
--- /dev/null
+++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then
+
+    quickchick_CI_REF=master+adapting-numTok-new-api-pr11703
+    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b82388675c..eac8d86b0a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -11,6 +11,8 @@
 
 Notations:
 
+- Most operators on numerals have moved to file numTok.ml.
+
 - Types `precedence`, `parenRelation`, `tolerability` in
   `notgram_ops.ml` have been reworked. See `entry_level` and
   `entry_relative_level` in `constrexpr.ml`.
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index ad2f2f93e7..633913aac6 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -7,69 +7,75 @@ set -e
 
 dev/tools/check-overlays.sh
 
-if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh ||
-        ! git diff-index --check --cached HEAD >/dev/null 2>&1 ;
+# Can we check and fix formatting?
+# NB: we will ignore errors from ocamlformat as it fails when
+# encountering OCaml syntax errors
+ocamlformat=$(command -v ocamlformat || echo true)
+if [ "$ocamlformat" = true ]
 then
-    1>&2 echo "Auto fixing whitespace issues..."
+    1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting."
+fi
 
-    # We fix whitespace in the index and in the working tree
-    # separately to preserve non-added changes.
-    index=$(mktemp "git-fix-ws-index.XXXXXX")
-    fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX")
-    tree=$(mktemp "git-fix-ws-tree.XXXXXX")
-    1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'."
-    1>&2 echo "If an error destroys your changes you can recover using them."
-    1>&2 echo "(The files are cleaned up on success.)"
-    1>&2 echo #newline
+1>&2 echo "Auto fixing whitespace and formatting issues..."
 
-    git diff-index -p --cached HEAD > "$index"
-    git diff-index -p HEAD > "$tree"
+# We fix whitespace in the index and in the working tree
+# separately to preserve non-added changes.
+index=$(mktemp "git-fix-ws-index.XXXXXX")
+fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX")
+tree=$(mktemp "git-fix-ws-tree.XXXXXX")
+1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'."
+1>&2 echo "If an error destroys your changes you can recover using them."
+1>&2 echo "(The files are cleaned up on success.)"
+1>&2 echo #newline
 
-    # reset work tree and index
-    # NB: untracked files which were not added are untouched
-    git apply --whitespace=nowarn --cached -R "$index"
-    git apply --whitespace=nowarn -R "$tree"
+git diff-index -p --cached HEAD > "$index"
+git diff-index -p HEAD > "$tree"
 
-    # Fix index
-    # For end of file newlines we must go through the worktree
+# reset work tree and index
+# NB: untracked files which were not added are untouched
+if [ -s "$index" ]; then git apply --whitespace=nowarn --cached -R "$index"; fi
+if [ -s "$tree" ]; then git apply --whitespace=nowarn -R "$tree"; fi
+
+# Fix index
+# For end of file newlines we must go through the worktree
+if [ -s "$index" ]; then
     1>&2 echo "Fixing staged changes..."
     git apply --cached --whitespace=fix "$index"
     git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
     git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
     git add -u
     1>&2 echo #newline
+fi
 
-    # reset work tree
-    git diff-index -p --cached HEAD > "$fixed_index"
-    # If all changes were bad whitespace changes the patch is empty
-    # making git fail. Don't fail now: we fix the worktree first.
-    if [ -s "$fixed_index" ]
-    then
-        git apply --whitespace=nowarn -R "$fixed_index"
-    fi
+# reset work tree
+git diff-index -p --cached HEAD > "$fixed_index"
+# If all changes were bad whitespace changes the patch is empty
+# making git fail. Don't fail now: we fix the worktree first.
+if [ -s "$fixed_index" ]; then git apply --whitespace=nowarn -R "$fixed_index"; fi
 
-    # Fix worktree
+# Fix worktree
+if [ -s "$tree" ]; then
     1>&2 echo "Fixing unstaged changes..."
     git apply --whitespace=fix "$tree"
     git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
     1>&2 echo #newline
+fi
 
-    if ! [ -s "$fixed_index" ]
-    then
-        1>&2 echo "No changes after fixing whitespace issues!"
-        exit 1
-    fi
-
-    # Check that we did fix whitespace
-    if ! git diff-index --check --cached HEAD;
-    then
-        1>&2 echo "Auto-fixing whitespace failed: errors remain."
-        1>&2 echo "This may fix itself if you try again."
-        1>&2 echo "(Consider whether the number of errors decreases after each run.)"
-        exit 1
-    fi
-    1>&2 echo "Whitespace issues fixed!"
+if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then
+    1>&2 echo "Fixing whitespace and formatting issues cancelled all changes."
+    exit 1
+fi
 
-    # clean up temporary files
-    rm "$index" "$tree" "$fixed_index"
+# Check that we did fix whitespace
+if ! git diff-index --check --cached HEAD; then
+    1>&2 echo "Auto-fixing whitespace failed: errors remain."
+    1>&2 echo "This may fix itself if you try again."
+    1>&2 echo "(Consider whether the number of errors decreases after each run.)"
+    exit 1
 fi
+1>&2 echo "Whitespace and formatting pass complete."
+
+# clean up temporary files
+rm "$index" "$tree" "$fixed_index"
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index da224aa5ab..06db787488 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -24,6 +24,8 @@ install_printer Top_printers.ppglob_constr
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppfconstr
 install_printer Top_printers.ppbigint
+install_printer Top_printers.ppnumtokunsigned
+install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
 install_printer Top_printers.ppidset
 install_printer Top_printers.ppidmapgen
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 96dbf9142b..7002cbffac 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -86,6 +86,8 @@ let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x)
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
+let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
+let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
 let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
 let ppintset l = pp (prset int (Int.Set.elements l))
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c5f97f5873..c826391cac 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -54,6 +54,8 @@ val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
 
 val ppbigint : Bigint.bigint -> unit
+val ppnumtokunsigned : NumTok.Unsigned.t -> unit
+val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit
 
 val ppintset : Int.Set.t -> unit
 val ppidset : Names.Id.Set.t -> unit