Refresh patches

4 files changed, 207 insertions, 503 deletions

diff --git a/debian/patches/python-scripts-libraries.patch b/debian/patches/python-scripts-libraries.patch
index 66a4a9e9..c4f662a8 100644
--- a/debian/patches/python-scripts-libraries.patch
+++ b/debian/patches/python-scripts-libraries.patch
@@ -5,7 +5,7 @@ Forwarded: not-needed
 Eliminate the .py extension from executable Python scripts.
 --- a/tools/CoqMakefile.in
 +++ b/tools/CoqMakefile.in
-@@ -91,9 +91,9 @@
+@@ -90,9 +90,9 @@
  COQMKFILE ?= "$(COQBIN)coq_makefile"
  
  # Timing scripts
diff --git a/debian/patches/remove-tests-that-need-coqlib.patch b/debian/patches/remove-tests-that-need-coqlib.patch
index 48cd1b96..be694991 100644
--- a/debian/patches/remove-tests-that-need-coqlib.patch
+++ b/debian/patches/remove-tests-that-need-coqlib.patch
@@ -1,6 +1,5 @@
 From: Benjamin Barenblat <bbaren@debian.org>
 Subject: Disable tests which require -coqlib to be set
-Bug: https://github.com/coq/coq/issues/5975
 Forwarded: not-needed
 
 A number of tests (mostly for coq_makefile) assume that Coq is
@@ -8,10 +7,9 @@ installed when the test runs. This isn't true in an sbuild environment,
 though, so disable those tests.
 --- a/test-suite/misc/printers.sh
 +++ /dev/null
-@@ -1,3 +0,0 @@
--printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound"
--if [ $? = 0 ]; then exit 1; else exit 0; fi
--
+@@ -1,2 +0,0 @@
+-#!/bin/sh
+-if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi
 --- a/test-suite/coq-makefile/arg/run.sh
 +++ /dev/null
 @@ -1,7 +0,0 @@
@@ -33,9 +31,96 @@ though, so disable those tests.
 -cat Makefile.conf
 -make
 -exec test -f "subdir/done"
+--- a/test-suite/coq-makefile/emptyprefix/run.sh
++++ /dev/null
+@@ -1,17 +0,0 @@
+-#!/usr/bin/env bash
+-
+-set -e
+-
+-. ../template/init.sh
+-
+-mv theories/sub theories2
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-
+-cp ../_CoqProject.sub theories2/_CoqProject
+-cd theories2
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+--- a/test-suite/coq-makefile/extend-subdirs/run.sh
++++ /dev/null
+@@ -1,8 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-exec test -f "subdir/done"
+--- a/test-suite/coq-makefile/latex1/run.sh
++++ /dev/null
+@@ -1,13 +0,0 @@
+-#!/usr/bin/env bash
+-
+-if which pdflatex; then
+-
+-. ../template/init.sh
+-	
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-exec make all.pdf
+-
+-fi
+-exit 0 # test skipped
+--- a/test-suite/coq-makefile/merlin1/run.sh
++++ /dev/null
+@@ -1,13 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make .merlin
+-cat > desired <<EOT
+-B src
+-S src
+-EOT
+-tail -2 .merlin > actual
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/only/run.sh
++++ /dev/null
+@@ -1,10 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make only TGTS="src/test.cmi src/test_aux.cmi" -j2
+-test -f src/test.cmi
+-test -f src/test_aux.cmi
+-! test -f src/test.cmo
+--- a/test-suite/coq-makefile/validate1/run.sh
++++ /dev/null
+@@ -1,8 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-exec make validate
 --- a/test-suite/coq-makefile/coqdoc1/run.sh
 +++ /dev/null
-@@ -1,51 +0,0 @@
+@@ -1,59 +0,0 @@
 -#!/usr/bin/env bash
 -
 -. ../template/init.sh
@@ -47,7 +132,15 @@ though, so disable those tests.
 -make install DSTROOT="$PWD/tmp"
 -make install-doc DSTROOT="$PWD/tmp"
 -#make debug
--(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
+-
+-# to learn about <(cmd) see https://www.gnu.org/software/bash/manual/html_node/Process-Substitution.html
+-(
+-  while IFS= read -r -d '' d
+-  do
+-    pushd "$d" >/dev/null && find . && popd >/dev/null
+-  done < <(find tmp -name user-contrib -print0)
+-) | sort -u > actual
+-
 -sort -u > desired <<EOT
 -.
 -./test
@@ -89,7 +182,7 @@ though, so disable those tests.
 -exec diff -u desired actual
 --- a/test-suite/coq-makefile/coqdoc2/run.sh
 +++ /dev/null
-@@ -1,51 +0,0 @@
+@@ -1,57 +0,0 @@
 -#!/usr/bin/env bash
 -
 -. ../template/init.sh
@@ -101,7 +194,13 @@ though, so disable those tests.
 -make install DSTROOT="$PWD/tmp"
 -make install-doc DSTROOT="$PWD/tmp"
 -#make debug
--(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
+-(
+-  while IFS= read -r -d '' d
+-  do
+-    pushd "$d" >/dev/null && find . && popd >/dev/null
+-  done < <(find tmp -name user-contrib -print0)
+-) | sort -u > actual
+-
 -sort -u > desired <<EOT
 -.
 -./test
@@ -141,40 +240,9 @@ though, so disable those tests.
 -./test/html/test.test.html
 -EOT
 -exec diff -u desired actual
---- a/test-suite/coq-makefile/emptyprefix/run.sh
-+++ /dev/null
-@@ -1,17 +0,0 @@
--#!/usr/bin/env bash
--
--set -e
--
--. ../template/init.sh
--
--mv theories/sub theories2
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
--
--cp ../_CoqProject.sub theories2/_CoqProject
--cd theories2
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
---- a/test-suite/coq-makefile/extend-subdirs/run.sh
-+++ /dev/null
-@@ -1,8 +0,0 @@
--#!/usr/bin/env bash
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
--exec test -f "subdir/done"
 --- a/test-suite/coq-makefile/findlib-package/run.sh
 +++ /dev/null
-@@ -1,18 +0,0 @@
+@@ -1,19 +0,0 @@
 -#!/usr/bin/env bash
 -
 -. ../template/init.sh
@@ -184,7 +252,8 @@ though, so disable those tests.
 -if which cygpath 2>/dev/null; then
 -  # the only way I found to pass OCAMLPATH on win is to have it contain
 -  # only one entry
--  export OCAMLPATH=`cygpath -w $PWD/findlib`
+-  OCAMLPATH=$(cygpath -w "$PWD"/findlib)
+-  export OCAMLPATH
 -fi
 -make -C findlib/foo clean
 -coq_makefile -f _CoqProject -o Makefile
@@ -193,38 +262,6 @@ though, so disable those tests.
 -make -C findlib/foo
 -make
 -make byte
---- a/test-suite/coq-makefile/latex1/run.sh
-+++ /dev/null
-@@ -1,13 +0,0 @@
--#!/usr/bin/env bash
--
--if which pdflatex; then
--
--. ../template/init.sh
--	
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
--exec make all.pdf
--
--fi
--exit 0 # test skipped
---- a/test-suite/coq-makefile/merlin1/run.sh
-+++ /dev/null
-@@ -1,13 +0,0 @@
--#!/usr/bin/env bash
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make .merlin
--cat > desired <<EOT
--B src
--S src
--EOT
--tail -2 .merlin > actual
--exec diff -u desired actual
 --- a/test-suite/coq-makefile/mlpack1/run.sh
 +++ /dev/null
 @@ -1,23 +0,0 @@
@@ -238,7 +275,7 @@ though, so disable those tests.
 -make html mlihtml
 -make install DSTROOT="$PWD/tmp"
 -#make debug
--(cd `find tmp -name user-contrib` && find .) | sort > actual
+-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual
 -sort > desired <<EOT
 -.
 -./test
@@ -264,7 +301,7 @@ though, so disable those tests.
 -make html mlihtml
 -make install DSTROOT="$PWD/tmp"
 -#make debug
--(cd `find tmp -name user-contrib` && find .) | sort > actual
+-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual
 -sort > desired <<EOT
 -.
 -./test
@@ -279,7 +316,7 @@ though, so disable those tests.
 -exec diff -u desired actual
 --- a/test-suite/coq-makefile/multiroot/run.sh
 +++ /dev/null
-@@ -1,56 +0,0 @@
+@@ -1,61 +0,0 @@
 -#!/usr/bin/env bash
 -
 -. ../template/init.sh
@@ -293,7 +330,12 @@ though, so disable those tests.
 -make install DSTROOT="$PWD/tmp"
 -make install-doc DSTROOT="$PWD/tmp"
 -#make debug
--(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
+-(
+-  while IFS= read -r -d '' d
+-  do
+-    pushd "$d" >/dev/null && find . && popd >/dev/null
+-  done < <(find tmp -name user-contrib -print0)
+-) | sort -u > actual
 -sort > desired <<EOT
 -.
 -./test
@@ -336,19 +378,6 @@ though, so disable those tests.
 -./orphan_test_test2_test/mlihtml/type_Test.html
 -EOT
 -exec diff -u desired actual
---- a/test-suite/coq-makefile/only/run.sh
-+++ /dev/null
-@@ -1,10 +0,0 @@
--#!/usr/bin/env bash
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make only TGTS="src/test.cmi src/test_aux.cmi" -j2
--test -f src/test.cmi
--test -f src/test_aux.cmi
--! test -f src/test.cmo
 --- a/test-suite/coq-makefile/plugin1/run.sh
 +++ /dev/null
 @@ -1,26 +0,0 @@
@@ -363,7 +392,7 @@ though, so disable those tests.
 -make html mlihtml
 -make install DSTROOT="$PWD/tmp"
 -#make debug
--(cd `find tmp -name user-contrib` && find .) | sort > actual
+-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual
 -sort > desired <<EOT
 -.
 -./test
@@ -392,7 +421,7 @@ though, so disable those tests.
 -make html mlihtml
 -make install DSTROOT="$PWD/tmp"
 -#make debug
--(cd `find tmp -name user-contrib` && find .) | sort > actual
+-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual
 -sort > desired <<EOT
 -.
 -./test
@@ -421,7 +450,7 @@ though, so disable those tests.
 -make html mlihtml
 -make install DSTROOT="$PWD/tmp"
 -#make debug
--(cd `find tmp -name user-contrib` && find .) | sort > actual
+-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual
 -sort > desired <<EOT
 -.
 -./test
@@ -440,89 +469,20 @@ though, so disable those tests.
 +++ /dev/null
 @@ -1,12 +0,0 @@
 -#!/usr/bin/env bash
--a=`uname`
+-a=$(uname)
 -
 -. ../template/init.sh
 -
 -coq_makefile -f _CoqProject -o Makefile
 -# vio2vo is broken on Windows (#6720)
--if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then
+-if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then
 -    make quick2vo J=2
 -    test -f theories/test.vo
 -    make validate
 -fi
---- a/test-suite/coq-makefile/uninstall1/run.sh
-+++ /dev/null
-@@ -1,18 +0,0 @@
--#!/usr/bin/env bash
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
--make html mlihtml
--make install DSTROOT="$PWD/tmp"
--make install-doc DSTROOT="$PWD/tmp"
--make uninstall DSTROOT="$PWD/tmp"
--make uninstall-doc DSTROOT="$PWD/tmp"
--#make debug
--(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
--sort -u > desired <<EOT
--.
--EOT
--exec diff -u desired actual
---- a/test-suite/coq-makefile/uninstall2/run.sh
-+++ /dev/null
-@@ -1,18 +0,0 @@
--#!/usr/bin/env bash
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
--make html mlihtml
--make install DSTROOT="$PWD/tmp"
--make install-doc DSTROOT="$PWD/tmp"
--make uninstall DSTROOT="$PWD/tmp"
--make uninstall-doc DSTROOT="$PWD/tmp"
--#make debug
--(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
--sort -u > desired <<EOT
--.
--EOT
--exec diff -u desired actual
---- a/test-suite/coq-makefile/validate1/run.sh
-+++ /dev/null
-@@ -1,8 +0,0 @@
--#!/usr/bin/env bash
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--cat Makefile.conf
--make
--exec make validate
---- a/test-suite/coq-makefile/vio2vo/run.sh
-+++ /dev/null
-@@ -1,13 +0,0 @@
--#!/usr/bin/env bash
--a=`uname`
--
--. ../template/init.sh
--
--coq_makefile -f _CoqProject -o Makefile
--make quick
--# vio2vo is broken on Windows (#6720)
--if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then
--    make vio2vo J=2
--    test -f theories/test.vo
--    make validate
--fi
 --- a/test-suite/coq-makefile/timing/run.sh
 +++ /dev/null
-@@ -1,108 +0,0 @@
+@@ -1,105 +0,0 @@
 -#!/usr/bin/env bash
 -
 -#set -x
@@ -587,16 +547,14 @@ though, so disable those tests.
 -    -e s'/  */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
 -    )
 -
--for ext in "" .desired; do
--    for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
--        cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed
--    done
--done
 -for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
--    echo "cat $file"
--    cat "$file"
--    echo
--    diff -u $file.desired.processed $file.processed || exit $?
+-  for ext in "" .desired; do
+-    grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed
+-  done
+-  echo "cat $file"
+-  cat "$file"
+-  echo
+-  diff -u $file.desired.processed $file.processed || exit $?
 -done
 -
 -cd ../per-file-before
@@ -621,13 +579,80 @@ though, so disable those tests.
 -cat A.v.timing.diff
 -echo
 -
+-file=A.v.timing.diff
+-
 -for ext in "" .desired; do
--    for file in A.v.timing.diff; do
--        cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed
--    done
--done
--for file in A.v.timing.diff; do
--    diff -u $file.desired.processed $file.processed || exit $?
+-    sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed"
 -done
 -
+-diff -u "$file.desired.processed" "$file.processed" || exit $?
+-
 -exit 0
+--- a/test-suite/coq-makefile/uninstall1/run.sh
++++ /dev/null
+@@ -1,23 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-make html mlihtml
+-make install DSTROOT="$PWD/tmp"
+-make install-doc DSTROOT="$PWD/tmp"
+-make uninstall DSTROOT="$PWD/tmp"
+-make uninstall-doc DSTROOT="$PWD/tmp"
+-#make debug
+-(
+-  while IFS= read -r -d '' d
+-  do
+-    pushd "$d" >/dev/null && find . && popd >/dev/null
+-  done < <(find tmp -name user-contrib -print0)
+-) | sort -u > actual
+-sort -u > desired <<EOT
+-.
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/uninstall2/run.sh
++++ /dev/null
+@@ -1,23 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-make html mlihtml
+-make install DSTROOT="$PWD/tmp"
+-make install-doc DSTROOT="$PWD/tmp"
+-make uninstall DSTROOT="$PWD/tmp"
+-make uninstall-doc DSTROOT="$PWD/tmp"
+-#make debug
+-(
+-  while IFS= read -r -d '' d
+-  do
+-    pushd "$d" >/dev/null && find . && popd >/dev/null
+-  done < <(find tmp -name user-contrib -print0)
+-) | sort -u > actual
+-sort -u > desired <<EOT
+-.
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/vio2vo/run.sh
++++ /dev/null
+@@ -1,13 +0,0 @@
+-#!/usr/bin/env bash
+-a=$(uname)
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-make quick
+-# vio2vo is broken on Windows (#6720)
+-if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then
+-    make vio2vo J=2
+-    test -f theories/test.vo
+-    make validate
+-fi
diff --git a/debian/patches/series b/debian/patches/series
index 2bf642fb..85f4fddd 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -3,7 +3,6 @@ Remove-test-4429.patch
 Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
 5127-fails-on-mips.patch
 remove-tests-that-need-coqlib.patch
-spelling.patch
 avoid-usr-bin-env.patch
 python-scripts-libraries.patch
 skip-dot-pc.patch
diff --git a/debian/patches/spelling.patch b/debian/patches/spelling.patch
deleted file mode 100644
index 149d11b4..00000000
--- a/debian/patches/spelling.patch
+++ /dev/null
@@ -1,320 +0,0 @@
-From: Benjamin Barenblat <bbaren@google.com>
-Subject: Correct some spelling errors
-Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca
-Reviewed-by: Benjamin Barenblat <bbaren@debian.org>
-
-Lintian found some spelling errors in the Debian packaging for coq. Fix
-them most places they appear in the current source. (Don't change
-documentation anchor names, as that would invalidate external
-deeplinks.)
-
-This also fixes a bug in coqdoc: prior to this commit, coqdoc would
-highlight `instanciate` but not `instantiate`.
---- a/ide/nanoPG.ml
-+++ b/ide/nanoPG.ml
-@@ -189,7 +189,7 @@
-       run "Edit" "Cut";
-       { s with kill = Some(txt,false); sel = false }
-     else s));
--  mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
-+  mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ ->
-     let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
-     let k =
-       if i#ends_line then begin
---- a/kernel/clambda.ml
-+++ b/kernel/clambda.ml
-@@ -767,7 +767,7 @@
-                               and such, which can't be done at this time.
-                               for instance, for int31: if one of the digit is
-                                   not closed, it's not impossible that the number
--                                  gets fully instanciated at run-time, thus to ensure
-+                                  gets fully instantiated at run-time, thus to ensure
-                                   uniqueness of the representation in the vm
-                                   it is necessary to try and build a caml integer
-                                   during the execution *)
---- a/lib/future.ml
-+++ b/lib/future.ml
-@@ -49,7 +49,7 @@
- module UUIDMap = Map.Make(UUID)
- module UUIDSet = Set.Make(UUID)
- 
--type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
-+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
- 
- (* Val is not necessarily a final state, so the
-    computation restarts from the state stocked into Val *)
-@@ -103,7 +103,7 @@
- let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
- 
- let create_delegate ?(blocking=true) ~name fix_exn =
--  let assignement signal ck = fun v ->
-+  let assignment signal ck = fun v ->
-     let _, _, fix_exn, c = get ck in
-     assert (match !c with Delegated _ -> true | _ -> false);
-     begin match v with
-@@ -118,7 +118,7 @@
-     (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
-     (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
-   let ck = create ~name fix_exn (Delegated wait) in
--  ck, assignement signal ck
-+  ck, assignment signal ck
- 
- (* TODO: get rid of try/catch to be stackless *)
- let rec compute ck : 'a value =
---- a/lib/future.mli
-+++ b/lib/future.mli
-@@ -70,10 +70,10 @@
- (* Run remotely, returns the function to assign.
-    If not blocking (the default) it raises NotReady if forced before the
-    delegate assigns it. *)
--type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
-+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
- val create_delegate :
-   ?blocking:bool -> name:string ->
--  fix_exn -> 'a computation * ('a assignement -> unit)
-+  fix_exn -> 'a computation * ('a assignment -> unit)
- 
- (* Given a computation that is_exn, replace it by another one *)
- val replace : 'a computation -> 'a computation -> unit
---- a/plugins/funind/functional_principles_proofs.ml
-+++ b/plugins/funind/functional_principles_proofs.ml
-@@ -638,11 +638,11 @@
- (*     observe (str "using snd tac since : " ++ CErrors.print e); *)
-     tac2 g
- 
--let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
-+let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
-   let args = Array.of_list (List.map mkVar  args_id) in
--  let instanciate_one_hyp hid =
-+  let instantiate_one_hyp hid =
-     my_orelse
--      ( (* we instanciate the hyp if possible  *)
-+      ( (* we instantiate the hyp if possible  *)
- 	fun g ->
- 	  let prov_hid = pf_get_new_id hid g in
- 	  let c = mkApp(mkVar hid,args) in
-@@ -678,7 +678,7 @@
-     tclTHENLIST
-       [
- 	tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
--	tclMAP instanciate_one_hyp hyps;
-+        tclMAP instantiate_one_hyp hyps;
- 	(fun g ->
- 	   let all_g_hyps_id =
- 	     List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
-@@ -722,11 +722,11 @@
- 			 tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
- 				     (fun g' ->
- 					let g'_nb_prod = nb_prod (project g') (pf_concl g') in
--					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
-+                                        let nb_instantiate_partial = g'_nb_prod - g_nb_prod in
- 			 		observe_tac "treat_new_case"
- 					  (treat_new_case
- 					     ptes_infos
--					     nb_instanciate_partial
-+                                             nb_instantiate_partial
- 					     (build_proof do_finalize)
- 					     t
- 					     dyn_infos)
-@@ -760,7 +760,7 @@
- 				  nb_rec_hyps  = List.length new_hyps
- 			       }
- 			   in
--(* 			   observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
-+(* 			   observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
- 			     (* 			   build_proof do_finalize new_infos g' *)
- 			) g
- 		  | _ ->
-@@ -1118,7 +1118,7 @@
- 	in
- 	(full_params, (* real params *)
- 	 princ_params, (* the params of the principle which are not params of the function *)
--	 substl (* function instanciated with real params *)
-+         substl (* function instantiated with real params *)
- 	   (List.map var_of_decl full_params)
- 	   f_body
- 	)
-@@ -1128,7 +1128,7 @@
- 	let f_body = compose_lam f_ctxt_other f_body in
- 	(princ_info.params, (* real params *)
- 	 [],(* all params are full params *)
--	 substl (* function instanciated with real params *)
-+         substl (* function instantiated with real params *)
- 	   (List.map var_of_decl princ_info.params)
- 	   f_body
- 	)
-@@ -1319,7 +1319,7 @@
- (* 			   str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
- 
- (* 			   ); *)
--		     (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac
-+                     (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac
- 		       (List.rev_map id_of_decl princ_info.branches)
- 		       (List.rev args_id))
- 		   ]
-@@ -1369,7 +1369,7 @@
- 			 do_prove
- 			 dyn_infos
- 		    in
--		    instanciate_hyps_with_args prove_tac
-+                    instantiate_hyps_with_args prove_tac
- 		       (List.rev_map id_of_decl princ_info.branches)
- 		      (List.rev args_id)
- 		   ]
-@@ -1726,8 +1726,8 @@
- 	     ptes_info
- 	     (body_info rec_hyps)
- 	 in
--	 (* observe_tac "instanciate_hyps_with_args"  *)
--	   (instanciate_hyps_with_args
-+         (* observe_tac "instantiate_hyps_with_args"  *)
-+           (instantiate_hyps_with_args
- 	      make_proof
- 	      (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
- 	      (List.rev args_ids)
---- a/plugins/funind/recdef.ml
-+++ b/plugins/funind/recdef.ml
-@@ -1318,7 +1318,7 @@
-     | None   ->
- 	try add_suffix current_proof_name "_subproof"
- 	with e when CErrors.noncritical e ->
--          anomaly (Pp.str "open_new_goal with an unamed theorem.")
-+          anomaly (Pp.str "open_new_goal with an unnamed theorem.")
-   in
-   let na = next_global_ident_away name Id.Set.empty in
-   if Termops.occur_existential sigma gls_type then
---- a/plugins/omega/PreOmega.v
-+++ b/plugins/omega/PreOmega.v
-@@ -181,7 +181,7 @@
-         let t := eval compute in (Z.of_nat (S a)) in
-         change (Z.of_nat (S a)) with t in H
-       | _ => rewrite (Nat2Z.inj_succ a) in H
--      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
-+      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
-                 hide [Z.of_nat (S a)] in this one hypothesis *)
-         change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
-      end
-@@ -192,7 +192,7 @@
-         let t := eval compute in (Z.of_nat (S a)) in
-         change (Z.of_nat (S a)) with t
-       | _ => rewrite (Nat2Z.inj_succ a)
--      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
-+      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
-                 hide [Z.of_nat (S a)] in the goal *)
-         change (Z.of_nat (S a)) with (Z_of_nat' (S a))
-      end
---- a/plugins/omega/omega.ml
-+++ b/plugins/omega/omega.ml
-@@ -178,7 +178,7 @@
-       | DIVIDE_AND_APPROX (e1,e2,k,d) ->
-           Printf.printf
-             "Inequation E%d is divided by %s and the constant coefficient is \
--            rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
-+            rounded by subtracting %s.\n" e1.id (sbi k) (sbi d)
-       | NOT_EXACT_DIVIDE (e,k) ->
-           Printf.printf
-             "Constant in equation E%d is not divisible by the pgcd \
---- a/stm/stm.ml
-+++ b/stm/stm.ml
-@@ -1343,7 +1343,7 @@
-     t_stop     : Stateid.t;
-     t_drop     : bool;
-     t_states   : competence;
--    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
-+    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
-     t_loc      : Loc.t option;
-     t_uuid     : Future.UUID.t;
-     t_name     : string }
-@@ -1381,7 +1381,7 @@
-     t_stop     : Stateid.t;
-     t_drop     : bool;
-     t_states   : competence;
--    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
-+    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
-     t_loc      : Loc.t option;
-     t_uuid     : Future.UUID.t;
-     t_name     : string }
-@@ -1819,7 +1819,7 @@
-   type task = {
-     t_state    : Stateid.t;
-     t_state_fb : Stateid.t;
--    t_assign   : output Future.assignement -> unit;
-+    t_assign   : output Future.assignment -> unit;
-     t_ast      : int * aast;
-     t_goal     : Goal.goal;
-     t_kill     : unit -> unit;
-@@ -1836,7 +1836,7 @@
-   type task = {
-     t_state    : Stateid.t;
-     t_state_fb : Stateid.t;
--    t_assign   : output Future.assignement -> unit;
-+    t_assign   : output Future.assignment -> unit;
-     t_ast      : int * aast;
-     t_goal     : Goal.goal;
-     t_kill     : unit -> unit;
---- a/test-suite/success/univers.v
-+++ b/test-suite/success/univers.v
-@@ -60,7 +60,7 @@
- 
- Record U : Type := { A:=Type; a:A }.
- 
--(** Check assignement of sorts to inductives and records. *)
-+(** Check assignment of sorts to inductives and records. *)
- 
- Variable sh : list nat.
- 
---- a/tools/coq_makefile.ml
-+++ b/tools/coq_makefile.ml
-@@ -59,7 +59,7 @@
- \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
- \n as a dependencies of an already defined target \"foo\".\
- \n[-I dir]: look for Objective Caml dependencies in \"dir\"\
--\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
-+\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\
- \n  starting from \"physicalpath\". The logical path associated to the\
- \n  physical path is \"logicalpath\".\
- \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
---- a/tools/coqdoc/output.ml
-+++ b/tools/coqdoc/output.ml
-@@ -76,7 +76,7 @@
-     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
-       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
--      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
-+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto";
-       "quote"; "eexact"; "autorewrite";
-       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
-       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
---- a/tools/coqworkmgr.ml
-+++ b/tools/coqworkmgr.ml
-@@ -169,7 +169,7 @@
-     "-j",Arg.Set_int max_tokens, "max number of concurrent jobs";
-     "-d",Arg.Set debug, "do not detach (debug)"] in
-   let usage =
--    "Prints on stdout an env variable assignement to be picked up by coq\n"^
-+    "Prints on stdout an env variable assignment to be picked up by coq\n"^
-     "instances in order to limit the maximum number of concurrent workers.\n"^
-     "The default value is 2.\n"^
-     "Usage:" in
---- a/vernac/comProgramFixpoint.ml
-+++ b/vernac/comProgramFixpoint.ml
-@@ -254,7 +254,7 @@
-     interp_recursive ~cofix ~program_mode:true fixl ntns
-   in
-     (* Program-specific code *)
--    (* Get the interesting evars, those that were not instanciated *)
-+    (* Get the interesting evars, those that were not instantiated *)
-   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
-     (* Solve remaining evars *)
-   let evd = nf_evar_map_undefined evd in
---- a/vernac/obligations.ml
-+++ b/vernac/obligations.ml
-@@ -338,7 +338,7 @@
- let _ =
-   declare_bool_option
-     { optdepr  = false;
--      optname  = "Hidding of Program obligations";
-+      optname  = "Hiding of Program obligations";
-       optkey   = ["Hide";"Obligations"];
-       optread  = get_hide_obligations;
-       optwrite = set_hide_obligations; }