21 files changed, 169 insertions, 41 deletions
diff --git a/Makefile.dune b/Makefile.dune
index c338405f2c..1313ef5eac 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -18,7 +18,7 @@ help:
 	@echo "  - world:  build all public binaries and libraries"
 	@echo "  - watch:  build all public binaries and libraries [continuous build]"
 	@echo "  - check:  build all ML files as fast as possible"
-	@echo "  - test-suite: run Coq's test suite"
+	@echo "  - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]"
 	@echo ""
 	@echo "  Note: running ./configure is not recommended,"
 	@echo "        see dev/doc/build-system.dune.md for more info"
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 2de103a2ff..748f50b54b 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -615,12 +615,29 @@ let pr_ast fmt = function
 | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
 | ArgumentExt arg -> fprintf fmt "%a@\n" ArgumentExt.print_ast arg
 
-let () =
+let help () =
+  Format.eprintf "Usage: coqpp file.mlg@\n%!";
+  exit 1
+
+let parse () =
   let () =
-    if Array.length Sys.argv <> 2 then fatal "Expected exactly one command line argument"
+    if Array.length Sys.argv <> 2
+    then help ()
   in
-  let file = Sys.argv.(1) in
-  let output = Filename.chop_extension file ^ ".ml" in
+  match Sys.argv.(1) with
+  | "-help" | "--help" -> help ()
+  | file -> file
+
+let output_name file =
+  try
+    Filename.chop_extension file ^ ".ml"
+  with
+  | Invalid_argument _ ->
+    fatal "Input file must have an extension for coqpp [input.ext -> input.ml]"
+
+let () =
+  let file = parse () in
+  let output = output_name file in
   let ast = parse_file file in
   let chan = open_out output in
   let fmt = formatter_of_out_channel chan in
diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index d2e0ee89bf..1b2d6a73a2 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,4 +5,7 @@ ci_dir="$(dirname "$0")"
 
 git_download paramcoq
 
+# Typically flaky on our worker configuration
+# https://gitlab.com/coq/coq/-/jobs/1144081161
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples)
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index da3022644d..db51dc08b6 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -6,7 +6,7 @@ load_printer clib.cma
 load_printer dynlink.cma
 load_printer lib.cma
 load_printer gramlib.cma
-load_printer byterun.cma
+load_printer coqrun.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index de3d5a3d15..8ebd6b5073 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -10,17 +10,23 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune).
 
 ## Quick Start
 
-Usually, using the latest version of Dune is recommended, see
-`dune-project` for the minimum required version; type `dune build` to
-build the base Coq libraries. No call to `./configure` is needed.
+Usually, using the latest version of Dune is recommended, see the
+first line of the `dune-project` file for the minimum required
+version.
+
+It is strongly recommended that you use the helper targets available
+in `Makefile.dune`, `make -f Makefile.dune` will display help. Note
+that dune will call configure for you if needed, so no need to call
+`./configure` in the regular development workflow.
+
+`dune build @install` will build all the public Coq artifacts; `dune
+build` will build all the targets in the workspace, including tests
+and documentations.
 
 Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
 the make-based system.
 
-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
 also generate an `.install` file so files can be properly installed by
 package managers.
@@ -84,7 +90,11 @@ builds, please see below.
 
 ## Documentation and testing targets
 
-Coq's test-suite can be run with `dune runtest`.
+Coq's test-suite can be run with `dune runtest`; given that `dune`
+still invokes the test-suite makefile, the environment variable
+`NJOBS` will control the value of the `-j` option that is passed to
+make; common call `NJOBS=8 dune runtest`. This will be resolved in the
+future once the test suite is ported to Dune rules.
 
 There is preliminary support to build the API documentation and
 reference manual in HTML format, use `dune build {@doc,@refman-html}`
@@ -229,3 +239,17 @@ useful to Coq, some examples are:
   implicitly loaded plugins / vo files. See the "Running binaries
   [coqtop / coqide]" section above as to how to correctly call Coq's
   binaries.
+
+## Dune cheat sheet
+
+- `dune build` build all targets in the current workspace
+- `dune build @check` build all ML targets as fast as possible, setup merlin
+- `dune utop $dir` open a shell for libraries in `$dir`
+- `dune exec -- $file` build and execute binary `$file`, can be in path or be an specific name
+- `dune build _build/$context/$foo` build target `$foo$` in `$context`, with build dir layout
+- `dune build _build/install/$context/foo` build target `$foo$` in `$context`, with install dir layout
+
+### packaging:
+
+- `dune subst` generate metadata for a package to be installed / distributed, necessary for opam
+- `dune build -p $pkg` build a package in release mode
diff --git a/dev/dune b/dev/dune
index 9da06a3fab..d3ba5c7e3d 100644
--- a/dev/dune
+++ b/dev/dune
@@ -21,8 +21,8 @@
     %{lib:coq-core.clib:clib.cma}
     %{lib:coq-core.lib:lib.cma}
     %{lib:coq-core.kernel:kernel.cma}
-    %{lib:coq-core.vm:byterun.cma}
-    %{lib:coq-core.vm:../../stublibs/dllbyterun_stubs.so}
+    %{lib:coq-core.vm:coqrun.cma}
+    %{lib:coq-core.vm:../../stublibs/dllcoqrun_stubs.so}
     %{lib:coq-core.library:library.cma}
     %{lib:coq-core.engine:engine.cma}
     %{lib:coq-core.pretyping:pretyping.cma}
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index bc86020d56..dff9b1e9e6 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -6,7 +6,7 @@ load_printer clib.cma
 load_printer dynlink.cma
 load_printer lib.cma
 load_printer gramlib.cma
-load_printer byterun.cma
+load_printer coqrun.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/dune_db_409 b/dev/dune_db_409
index adb1f76872..6c9f701b65 100644
--- a/dev/dune_db_409
+++ b/dev/dune_db_409
@@ -5,7 +5,7 @@ load_printer config.cma
 load_printer clib.cma
 load_printer lib.cma
 load_printer gramlib.cma
-load_printer byterun.cma
+load_printer coqrun.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/doc/changelog/01-kernel/14004-vm-array-set.rst b/doc/changelog/01-kernel/14004-vm-array-set.rst
deleted file mode 100644
index f90d611f84..0000000000
--- a/doc/changelog/01-kernel/14004-vm-array-set.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set``
-  (`#14005 <https://github.com/coq/coq/pull/14005>`_,
-  fixes `#13998 <https://github.com/coq/coq/issues/13998>`_,
-  by Guillaume Melquiond).
diff --git a/doc/changelog/01-kernel/14007-fix-14006.rst b/doc/changelog/01-kernel/14007-fix-14006.rst
deleted file mode 100644
index 6765768295..0000000000
--- a/doc/changelog/01-kernel/14007-fix-14006.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Fixed:**
-  Never store persistent arrays as VM / native structured values.
-  This could be used to make vo marshalling crash, and probably
-  breaking some other invariants of the kernel
-  (`#14007 <https://github.com/coq/coq/pull/14007>`_,
-  fixes `#14006 <https://github.com/coq/coq/issues/14006>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/04-tactics/14012-ltac2-array-init.rst b/doc/changelog/04-tactics/14012-ltac2-array-init.rst
deleted file mode 100644
index c79fc7e29a..0000000000
--- a/doc/changelog/04-tactics/14012-ltac2-array-init.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  Ltac2 ``Array.init`` no longer incurs exponential overhead when used
-  recursively (`#14012 <https://github.com/coq/coq/pull/14012>`_, fixes `#14011
-  <https://github.com/coq/coq/issues/14011>`_, by Jason Gross).
diff --git a/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst
new file mode 100644
index 0000000000..6a34f5a70e
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Failure of extraction in the presence of inductive types with local
+  definitions in parameters
+  (`#13624 <https://github.com/coq/coq/pull/13624>`_,
+  fixes `#13581 <https://github.com/coq/coq/issues/13581>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 4f3ee2dcaf..bf8174f246 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -721,6 +721,33 @@ CoqIDE
   (`#13870 <https://github.com/coq/coq/pull/13870>`_,
   by Guillaume Melquiond).
 
+Changes in 8.13.2
+~~~~~~~~~~~~~~~~~
+
+Kernel
+^^^^^^
+
+- **Fixed:**
+  Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set``
+  (`#14005 <https://github.com/coq/coq/pull/14005>`_,
+  fixes `#13998 <https://github.com/coq/coq/issues/13998>`_,
+  by Guillaume Melquiond).
+- **Fixed:**
+  Never store persistent arrays as VM / native structured values.
+  This could be used to make vo marshalling crash, and probably
+  breaking some other invariants of the kernel
+  (`#14007 <https://github.com/coq/coq/pull/14007>`_,
+  fixes `#14006 <https://github.com/coq/coq/issues/14006>`_,
+  by Pierre-Marie Pédrot).
+
+Tactic language
+^^^^^^^^^^^^^^^^
+
+- **Fixed:**
+  Ltac2 ``Array.init`` no longer incurs exponential overhead when used
+  recursively (`#14012 <https://github.com/coq/coq/pull/14012>`_, fixes `#14011
+  <https://github.com/coq/coq/issues/14011>`_, by Jason Gross).
+
 
 Version 8.12
 ------------
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 5d36ec3cf9..49c2c6b785 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -515,6 +515,11 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use
   + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target
     (``.PHONY`` or not) please use ``CoqMakefile.local``.
 
+.. note::
+
+  Due to limitations with the compilation chain, makefiles generated
+  by ``coq_makefile`` won't correctly compile OCaml plugins with OCaml
+  < 4.07.0 when using more than one job (``-j N`` for ``N > 1``).
 
 Precompiling for ``native_compute``
 +++++++++++++++++++++++++++++++++++
diff --git a/ide/coqide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang
index fc7bc64a68..d71277f42c 100644
--- a/ide/coqide/coq-ssreflect.lang
+++ b/ide/coqide/coq-ssreflect.lang
@@ -32,7 +32,7 @@
     <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex>
     <define-regex id="undotted_sep">[-+*{}]</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
-    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
+    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Variant)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
     <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
     <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
     <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
diff --git a/ide/coqide/coq.lang b/ide/coqide/coq.lang
index e9eab48de7..e6e813aca2 100644
--- a/ide/coqide/coq.lang
+++ b/ide/coqide/coq.lang
@@ -29,7 +29,7 @@
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
     <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
-    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Variant|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex>
     <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
     <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
     <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 2d75ad9ff6..6e02d7fed1 100644
--- a/ide/coqide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
@@ -151,6 +151,7 @@ let commands = [
    "Unset Silent.";
    "Unset Undo";];
   ["Variable";
+   "Variant";
    "Variables";];
   ["Write State";];
 ]
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index b14ad5c558..4d2000bb52 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,5 +1,5 @@
 (library
- (name byterun)
+ (name coqrun)
  (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
  (public_name coq-core.vm)
  (foreign_stubs
diff --git a/kernel/dune b/kernel/dune
index 0bf51f80ec..af88e9864f 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -4,7 +4,7 @@
  (public_name coq-core.kernel)
  (wrapped false)
  (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
- (libraries lib byterun dynlink))
+ (libraries lib coqrun dynlink))
 
 (executable
   (name genOpcodeFiles)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ca4f5429a2..30f90dd1fc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -427,6 +427,7 @@ and extract_really_ind env kn mib =
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in
+    let ndecls = List.length mib.mind_params_ctxt in
     let npar = mib.mind_nparams in
     let epar = push_rel_context mib.mind_params_ctxt env in
     let sg = Evd.from_env env in
@@ -462,17 +463,17 @@ and extract_really_ind env kn mib =
       if not p.ip_logical then
         let types = arities_of_constructors env ((kn,i),u) in
         for j = 0 to Array.length types - 1 do
-          let t = snd (decompose_prod_n npar types.(j)) in
+          let t = snd (decompose_prod_n_assum ndecls types.(j)) in
           let prods,head = dest_prod epar t in
           let nprods = List.length prods in
           let args = match Constr.kind head with
             | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
-          let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
-          let db = db_from_ind dbmap npar in
+          let dbmap = parse_ind_args p.ip_sign args (nprods + ndecls) in
+          let db = db_from_ind dbmap ndecls in
           p.ip_types.(j) <-
-            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1)
+            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (ndecls+1)
         done
     done;
     (* Third pass: we determine special cases. *)
diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v
new file mode 100644
index 0000000000..910537cf11
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13581.v
@@ -0,0 +1,60 @@
+From Coq Require Extraction.
+
+Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }.
+Definition d := Mixin nat tt (fun x => x).
+
+Extraction TestCompile d.
+
+(* Extra tests *)
+
+Record R T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) := Build
+  { g : T0 -> let U:=T0 in U ; h : d = d ; x : nat ; y := x+x }.
+
+Definition r := {| g := (fun x : nat => x) ; h := eq_refl (eq_refl 0) ; x := 0 |}.
+
+Extraction TestCompile r.
+(*
+(** val r0 : nat r **)
+
+let r0 =
+  { g = (fun x0 -> x0); x = O }
+*)
+
+Inductive I T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall d (e:=S d) (h : S d = e), Type :=
+| C : I T a b 0 eq_refl
+| D : J T a b true eq_refl -> I T a b 1 eq_refl
+with J T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall (d:bool) (h:d = true), Type :=
+| E : I T a b 0 eq_refl -> J T a b true eq_refl.
+
+Definition c := D _ _ _ (E _ _ _ (C nat 0 0)).
+
+Extraction TestCompile c.
+
+(*
+(** val c : nat i **)
+
+let c =
+  D (E C)
+*)
+
+CoInductive V T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { k : T; b := c+e ; m : nat; z : option (W nat 0 0 eq_refl) }
+with W T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { l : V nat 0 0 eq_refl }.
+
+CoFixpoint v :=
+  {| k := 0 ; m := 0 ; z := Some w ; |}
+with w := {| l := v |}.
+
+Extraction TestCompile v.
+(*
+(** val v0 : nat v **)
+
+let rec v0 =
+  lazy (Build_V (O, O, (Some w0)))
+
+(** val w0 : nat w **)
+
+and w0 =
+  lazy (Build_W v0)
+*)