21 files changed, 165 insertions, 68 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 754c09776e..4f58dc5aac 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -828,7 +828,7 @@ plugin:ci-coq_dpdgraph:
   extends: .ci-template
 
 plugin:ci-coqhammer:
-  extends: .ci-template
+  extends: .ci-template-flambda
 
 plugin:ci-elpi:
   extends: .ci-template
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml
index 25545cf565..69136ee773 100644
--- a/dev/bench/gitlab-bench.yml
+++ b/dev/bench/gitlab-bench.yml
@@ -4,9 +4,7 @@ bench:
   when: manual
   before_script:
     - printenv -0 | sort -z | tr '\0' '\n'
-  script:
-    - . ~/.opam/opam-init/init.sh
-    - ./dev/bench/gitlab.sh
+  script: dev/bench/gitlab.sh
   tags:
     - timing
   variables:
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index b616371ef8..2ce3cb77be 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -52,7 +52,7 @@ check_variable "CI_JOB_URL"
 : "${new_coq_opam_archive_git_branch:=master}"
 : "${old_coq_opam_archive_git_branch:=master}"
 : "${num_of_iterations:=1}"
-: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial}"
+: "${coq_opam_packages:=coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial coq-vst}"
 
 new_coq_commit=$(git rev-parse HEAD^2)
 old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 894244044a..64053a62f9 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -63,13 +63,9 @@ in time.
   the update to the Credits chapter of the reference manual.
   See also [#7058](https://github.com/coq/coq/issues/7058).
 
-  The command that was used in the previous versions to get the list
-  of contributors for this version is `git shortlog -s -n
-  VX.X+alpha..master | cut -f2 | sort -k 2`. Note that the ordering is
-  approximative as it will misplace people with middle names. It is
-  also probably not correctly handling `Co-authored-by` info that we
-  have been using more lately, so should probably be updated to
-  account for this.
+  The `dev/tools/list-contributors.sh` script computes the number and
+  list of contributors between Coq revisions. Typically used with
+  `VX.X+alpha..vX.X` to check the contributors of version `VX.X`.
 
 ## On the date of the feature freeze ##
 
diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh
new file mode 100644
index 0000000000..c968f2e952
--- /dev/null
+++ b/dev/tools/list-contributors.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+# For compat with OSX which has a non-gnu sed which doesn't support -z
+SED=`which gsed || which sed`
+
+if [ $# != 1 ]; then
+  error "usage: $0 rev0..rev1"
+  exit 1
+fi
+
+git shortlog -s -n --group=author --group=trailer:Co-authored-by $1 | cut -f2 | sort -k 2 | grep -v -e "coqbot" -e "^$" > contributors.tmp
+
+cat contributors.tmp | wc -l | xargs echo "Contributors:"
+cat contributors.tmp | gsed -z "s/\n/, /g"
+echo
+rm contributors.tmp
diff --git a/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst b/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst
new file mode 100644
index 0000000000..e3375bd875
--- /dev/null
+++ b/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst
@@ -0,0 +1,3 @@
+- **Deprecated:**
+  The micromega option :flag:`Simplex`, which is currently set by default
+  (`#13781 <https://github.com/coq/coq/pull/13781>`_, by Frédéric Besson).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 3bd85d29c8..5d471c695c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -31,9 +31,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
 
 .. flag:: Simplex
 
+   .. deprecated:: 8.14
+
    This flag (set by default) instructs the decision procedures to
-   use the Simplex method for solving linear goals. If it is not set,
-   the decision procedures are using Fourier elimination.
+   use the Simplex method for solving linear goals instead of the
+   deprecated Fourier elimination.
 
 .. opt:: Dump Arith
 
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 8dbc1626ba..7566996ef6 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -9,7 +9,7 @@ Binders
 .. insertprodn open_binders binder
 
 .. prodn::
-   open_binders ::= {+ @name } : @term
+   open_binders ::= {+ @name } : @type
    | {+ @binder }
    name ::= _
    | @ident
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 663337bc64..f286533d78 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -44,11 +44,14 @@ Rewriting with Leibniz and setoid equality
       oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings
       one_term_with_bindings ::= {? > } @one_term {? with @bindings }
 
-   Rewrites terms based on equalities.  The type of :n:`@one_term` must have the form:
+   Replaces subterms with other subterms that have been proven to be equal.
+   The type of :n:`@one_term` must have the form:
 
       :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2`
 
-   where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality.
+   .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3.
+
+   where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`.
    Note that :n:`eq @term__1 @term__2` is typically written with the infix notation
    :n:`@term__1 = @term__2`.  You must `Require Setoid` to use the tactic
    with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`.
@@ -61,7 +64,7 @@ Rewriting with Leibniz and setoid equality
    Some of the variables :g:`x`\ :sub:`i` are solved by unification,
    and some of the types :n:`A__1, ..., A__n` may become new
    subgoals.  :tacn:`rewrite` won't find occurrences inside `forall` that refer
-   to variables bound by the `forall`; use :tacn:`setoid_rewrite`
+   to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite`
    if you want to find such occurrences.
 
    :n:`{+, @oriented_rewriter }`
@@ -90,15 +93,55 @@ Rewriting with Leibniz and setoid equality
      any of them can be rewritten.  If not specified, only the first occurrence
      in the conclusion is replaced.
 
-     If :n:`at @occs_nums` is specified, rewriting is always done with
-     :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality,
-     which means that you must `Require Setoid` to use that form.
-     However, note that :tacn:`rewrite` (even when using setoid rewriting) and
-     :tacn:`setoid_rewrite` don't behave identically (as already mentioned above).
+     .. note::
+
+        If :n:`at @occs_nums` is specified, rewriting is always done
+        with :ref:`setoid rewriting <generalizedrewriting>`, even for
+        Leibniz equality, which means that you must `Require
+        Setoid` to use that form.  However, note that :tacn:`rewrite`
+        (even when using setoid rewriting) and :tacn:`setoid_rewrite`
+        don't behave identically (as is noted above and below).
 
    :n:`by @ltac_expr3`
      If specified, is used to resolve all side conditions generated by the tactic.
 
+   .. note::
+
+      For each selected hypothesis and/or the conclusion,
+      :tacn:`rewrite` finds the first matching subterm in
+      depth-first search order. Only subterms identical to
+      that first matched subterm are rewritten.  If the `at` clause is specified,
+      only these subterms are considered when counting occurrences.
+      To select a different set of matching subterms, you can
+      specify how some or all of the free variables are bound by
+      using a `with` clause (see :n:`@one_term_with_bindings`).
+
+      For instance, if we want to rewrite the right-hand side in the
+      following goal, this will not work:
+
+      .. coqtop:: none
+
+         Require Import Arith.
+
+      .. coqtop:: out
+
+         Lemma example x y : x + y = y + x.
+
+      .. coqtop:: all fail
+
+         rewrite Nat.add_comm at 2.
+
+      One can explicitly specify how some variables are bound to match
+      a different subterm:
+
+      .. coqtop:: all abort
+
+         rewrite Nat.add_comm with (m := x).
+
+      Note that the more advanced :tacn:`setoid_rewrite` tactic
+      behaves differently, and thus the number of occurrences
+      available to rewrite may differ between the two tactics.
+
    .. exn:: Tactic failure: Setoid library not loaded.
       :undocumented:
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 8aeb2e564d..27144fd1ad 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -447,7 +447,7 @@ binder: [
 
 open_binders: [
 | REPLACE name LIST0 name ":" lconstr
-| WITH LIST1 name ":" lconstr
+| WITH LIST1 name ":" type
 (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
 | DELETE name ".." name
 | REPLACE name LIST0 name binders
@@ -1510,8 +1510,6 @@ query_command: [
 | WITH "Check" lconstr
 | REPLACE "About" smart_global OPT univ_name_list "."
 | WITH "About" smart_global OPT univ_name_list
-| REPLACE "SearchHead" constr_pattern in_or_out_modules "."
-| WITH "SearchHead" constr_pattern in_or_out_modules
 | REPLACE "SearchPattern" constr_pattern in_or_out_modules "."
 | WITH "SearchPattern" constr_pattern in_or_out_modules
 | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ec23ffe83e..bc6b803bbb 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -687,17 +687,6 @@ command: [
 | "Add" "Zify" "BinOpSpec" constr      (* micromega plugin *)
 | "Add" "Zify" "UnOpSpec" constr      (* micromega plugin *)
 | "Add" "Zify" "Saturate" constr      (* micromega plugin *)
-| "Add" "InjTyp" constr      (* micromega plugin *)
-| "Add" "BinOp" constr      (* micromega plugin *)
-| "Add" "UnOp" constr      (* micromega plugin *)
-| "Add" "CstOp" constr      (* micromega plugin *)
-| "Add" "BinRel" constr      (* micromega plugin *)
-| "Add" "PropOp" constr      (* micromega plugin *)
-| "Add" "PropBinOp" constr      (* micromega plugin *)
-| "Add" "PropUOp" constr      (* micromega plugin *)
-| "Add" "BinOpSpec" constr      (* micromega plugin *)
-| "Add" "UnOpSpec" constr      (* micromega plugin *)
-| "Add" "Saturate" constr      (* micromega plugin *)
 | "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | "Show" "Zify" "BinOp"      (* micromega plugin *)
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
@@ -705,7 +694,6 @@ command: [
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
-| "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" constr OPT ring_mods      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
@@ -1258,7 +1246,6 @@ query_command: [
 | "Compute" lconstr "."
 | "Check" lconstr "."
 | "About" smart_global OPT univ_name_list "."
-| "SearchHead" constr_pattern in_or_out_modules "."
 | "SearchPattern" constr_pattern in_or_out_modules "."
 | "SearchRewrite" constr_pattern in_or_out_modules "."
 | "Search" search_query search_queries "."
@@ -1551,7 +1538,6 @@ simple_tactic: [
 | "revert" LIST1 hyp
 | "simple" "induction" quantified_hypothesis
 | "simple" "destruct" quantified_hypothesis
-| "double" "induction" quantified_hypothesis quantified_hypothesis
 | "admit"
 | "fix" ident natural
 | "cofix" ident
@@ -1669,7 +1655,6 @@ simple_tactic: [
 | "autounfold_one" hintbases
 | "unify" constr constr
 | "unify" constr constr "with" preident
-| "convert_concl_no_check" constr
 | "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
 | "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
 | "typeclasses" "eauto" "bfs" OPT nat_or_var
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 75b32a5800..a34e96ac16 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -493,7 +493,7 @@ term_forall_or_fun: [
 ]
 
 open_binders: [
-| LIST1 name ":" term
+| LIST1 name ":" type
 | LIST1 binder
 ]
 
@@ -1001,18 +1001,6 @@ command: [
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
-| "Add" "InjTyp" one_term      (* micromega plugin *)
-| "Add" "BinOp" one_term      (* micromega plugin *)
-| "Add" "UnOp" one_term      (* micromega plugin *)
-| "Add" "CstOp" one_term      (* micromega plugin *)
-| "Add" "BinRel" one_term      (* micromega plugin *)
-| "Add" "PropOp" one_term      (* micromega plugin *)
-| "Add" "PropBinOp" one_term      (* micromega plugin *)
-| "Add" "PropUOp" one_term      (* micromega plugin *)
-| "Add" "BinOpSpec" one_term      (* micromega plugin *)
-| "Add" "UnOpSpec" one_term      (* micromega plugin *)
-| "Add" "Saturate" one_term      (* micromega plugin *)
-| "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
@@ -1117,7 +1105,6 @@ command: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
@@ -1626,7 +1613,6 @@ simple_tactic: [
 | "revert" LIST1 ident
 | "simple" "induction" [ ident | natural ]
 | "simple" "destruct" [ ident | natural ]
-| "double" "induction" [ ident | natural ] [ ident | natural ]
 | "admit"
 | "clear" LIST0 ident
 | "clear" "-" LIST1 ident
@@ -1758,7 +1744,6 @@ simple_tactic: [
 | "autounfold" OPT hintbases OPT occurrences
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
-| "convert_concl_no_check" one_term
 | "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident )
 | "head_of_constr" ident one_term
 | "not_evar" one_term
@@ -2420,7 +2405,6 @@ tac2mode: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index cc1fa647f9..ee7dab92bc 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -173,3 +173,9 @@ let create ~name ~category ?(default=Enabled) pp =
     | Disabled -> ()
     | AsError -> CErrors.user_err ?loc (pp x)
     | Enabled -> Feedback.msg_warning ?loc (pp x)
+
+(* Remark: [warn] does not need to start with a comma, but if present
+   it won't hurt (",," is normalized into ","). *)
+let with_warn warn (f:'b -> 'a) x =
+  let s = get_flags () in
+  Util.try_finally (fun x -> set_flags (s^","^warn);f x) x set_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index ded1f9be3b..b63eed09d0 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -19,3 +19,10 @@ val set_flags : string -> unit
 (** Cleans up a user provided warnings status string, e.g. removing unknown
     warnings (in which case a warning is emitted) or subsumed warnings . *)
 val normalize_flags_string : string -> string
+
+(** [with_warn "-xxx,+yyy..." f x] calls [f x] after setting the
+   warnings as specified in the string (keeping other previously set
+   warnings), and restores current warnings after [f()] returns or
+   raises an exception. If both f and restoring the warnings raise
+   exceptions, the latter is raised. *)
+val with_warn: string -> ('b -> 'a) -> 'b -> 'a
diff --git a/lib/util.ml b/lib/util.ml
index 87cc30e557..e8aa0f3e48 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a
 
 let delayed_force f = f ()
 
+(* finalize - Credit X.Leroy, D.Remy. *)
+let try_finally f x finally y =
+  let res = try f x with exn -> finally y; raise exn in
+  finally y;
+  res
+
+
 (* Misc *)
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index fe34525671..aefb015c38 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -112,6 +112,15 @@ type 'a delayed = unit -> 'a
 
 val delayed_force : 'a delayed -> 'a
 
+(** [try_finally f x g y] applies the main code [f] to [x] and
+   returns the result after having applied the finalization
+   code [g] to [y]. If the main code raises the exception
+   [exn], the finalization code is executed and [exn] is raised.
+   If the finalization code itself fails, the exception
+   returned is always the one from the finalization code.
+   Credit X.Leroy, D.Remy. *)
+val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b
+
 (** {6 Enriched exceptions} *)
 
 type iexn = Exninfo.iexn
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ca6ae150a7..15cf88f827 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -195,16 +195,29 @@ let is_interactive recsl =
 
 }
 
+(* For usability we temporarily switch off some flags during the call
+   to Function. However this is not satisfactory:
+
+ 1- Function should not warn "non-recursive" and call the Definition
+    mechanism instead of Fixpoint when needed
+
+ 2- Only for automatically generated names should
+    unused-pattern-matching-variable be ignored. *)
+
 VERNAC COMMAND EXTEND Function STATE CUSTOM
 | ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
     => { classify_funind recsl }
     -> {
-         if is_interactive recsl then
-           Vernacextend.VtOpenProof (fun () ->
-             Gen_principle.do_generate_principle_interactive (List.map snd recsl))
-         else
-           Vernacextend.VtDefault (fun () ->
-             Gen_principle.do_generate_principle (List.map snd recsl)) }
+    let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in
+    if is_interactive recsl then
+      Vernacextend.VtOpenProof (fun () ->
+          CWarnings.with_warn warn
+            Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+    else
+      Vernacextend.VtDefault (fun () ->
+          CWarnings.with_warn warn
+            Gen_principle.do_generate_principle (List.map snd recsl))
+  }
 END
 
 {
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 74d5374193..ed608bb1df 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -28,7 +28,7 @@ open Q.Notations
 open Mutils
 
 let use_simplex =
-  Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true
+  Goptions.declare_bool_option_and_ref ~depr:true ~key:["Simplex"] ~value:true
 
 (* If set to some [file], arithmetic goals are dumped in [file].v *)
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5e138fa3d1..91f7e27911 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -38,14 +38,14 @@ let max_depth = max_int
 
 (* Search limit for provers over Q R *)
 let lra_proof_depth =
-  declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth
+  declare_int_option_and_ref ~depr:true ~key:["Lra"; "Depth"] ~value:max_depth
 
 (* Search limit for provers over Z *)
 let lia_enum =
-  declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true
+  declare_bool_option_and_ref ~depr:true ~key:["Lia"; "Enum"] ~value:true
 
 let lia_proof_depth =
-  declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth
+  declare_int_option_and_ref ~depr:true ~key:["Lia"; "Depth"] ~value:max_depth
 
 let get_lia_option () =
   (Certificate.use_simplex (), lia_enum (), lia_proof_depth ())
diff --git a/test-suite/output/Function.out b/test-suite/output/Function.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/Function.out
diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v
new file mode 100644
index 0000000000..b3e2a93895
--- /dev/null
+++ b/test-suite/output/Function.v
@@ -0,0 +1,31 @@
+Require Import FunInd List.
+
+(* Explanations: This kind of pattern matching displays a legitimate
+   unused variable warning in v8.13.
+
+Fixpoint f (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | x :: l'  => f l'
+  end.
+*)
+
+(* In v8.13 the same code with "Function" generates a lot more
+   warnings about variables created automatically by Function. These
+   are not legitimate. PR #13776 (post v8.13) removes all warnings
+   about pattern matching variables (and non truly recursive fixpoint)
+   for "Function". So this should not generate any warning. Note that
+   this PR removes also the legitimate warnings. It would be better if
+   this test generate the same warning as the Fixpoint above. This
+   test would then need to be updated. *)
+
+(* Ensuring the warning is a warning. *)
+Set Warnings "matching-variable".
+(* But no warning generated here. *)
+Function f (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | n :: l'  => f l'
+  end.