Documentation of branch “master” at 702b8241

coq · Dec 13, 2024 · 6a0fea5 · 6a0fea5
1 parent 04dacb2
commit 6a0fea5
Show file tree

Hide file tree

Showing 328 changed files with 3,725 additions and 3,781 deletions.
diff --git a/master/api/coq-core/ComInductive/Internal/index.html b/master/api/coq-core/ComInductive/Internal/index.html
@@ -1,3 +1,3 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Internal (coq-core.ComInductive.Internal)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">coq-core</a> &#x00BB; <a href="../index.html">ComInductive</a> &#x00BB; Internal</nav><header class="odoc-preamble"><h1>Module <code><span>ComInductive.Internal</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-inductive_levels" class="anchored"><a href="#val-inductive_levels" class="anchor"></a><code><span><span class="keyword">val</span> inductive_levels : <span>auto_prop_lowering:bool <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Environ/index.html#type-env">Environ.env</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Evd/index.html#type-evar_map">Evd.evar_map</a> <span class="arrow">&#45;&gt;</span></span> <span>poly:bool <span class="arrow">&#45;&gt;</span></span> <span>indnames:<span><a href="../../Names/Id/index.html#type-t">Names.Id.t</a> list</span>
-<span class="arrow">&#45;&gt;</span></span> <span>arities_explicit:<span>bool list</span> <span class="arrow">&#45;&gt;</span></span> <span><span><a href="../../EConstr/index.html#type-constr">EConstr.constr</a> list</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span><a href="../../EConstr/index.html#type-rel_context">EConstr.rel_context</a> list</span> list</span> <span class="arrow">&#45;&gt;</span></span> <a href="../../Evd/index.html#type-evar_map">Evd.evar_map</a> * <span>(<span><a href="../../DeclareInd/index.html#type-default_dep_elim">DeclareInd.default_dep_elim</a> list</span> * <span><a href="../../EConstr/index.html#type-t">EConstr.t</a> list</span>)</span></span></code></div><div class="spec-doc"><p>Returns the modified arities (the result sort may be replaced by Prop). Should be called with minimized universes.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-error_differing_params" class="anchored"><a href="#val-error_differing_params" class="anchor"></a><code><span><span class="keyword">val</span> error_differing_params : <span>kind:string <span class="arrow">&#45;&gt;</span></span> <span><span>(<a href="../../Names/index.html#type-lident">Names.lident</a> * <a href="../../Vernacexpr/index.html#type-inductive_params_expr">Vernacexpr.inductive_params_expr</a>)</span> <span class="arrow">&#45;&gt;</span></span> <span><span>(<a href="../../Names/index.html#type-lident">Names.lident</a> * <a href="../../Vernacexpr/index.html#type-inductive_params_expr">Vernacexpr.inductive_params_expr</a>)</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div></div></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Internal (coq-core.ComInductive.Internal)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">coq-core</a> &#x00BB; <a href="../index.html">ComInductive</a> &#x00BB; Internal</nav><header class="odoc-preamble"><h1>Module <code><span>ComInductive.Internal</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-inductive_levels" class="anchored"><a href="#val-inductive_levels" class="anchor"></a><code><span><span class="keyword">val</span> inductive_levels : <span><a href="../../Environ/index.html#type-env">Environ.env</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Evd/index.html#type-evar_map">Evd.evar_map</a> <span class="arrow">&#45;&gt;</span></span> <span>poly:bool <span class="arrow">&#45;&gt;</span></span> <span>indnames:<span><a href="../../Names/Id/index.html#type-t">Names.Id.t</a> list</span> <span class="arrow">&#45;&gt;</span></span>
+<span>arities_explicit:<span>bool list</span> <span class="arrow">&#45;&gt;</span></span> <span><span><a href="../../EConstr/index.html#type-constr">EConstr.constr</a> list</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span><a href="../../EConstr/index.html#type-rel_context">EConstr.rel_context</a> list</span> list</span> <span class="arrow">&#45;&gt;</span></span> <a href="../../Evd/index.html#type-evar_map">Evd.evar_map</a> * <span>(<span><a href="../../DeclareInd/index.html#type-default_dep_elim">DeclareInd.default_dep_elim</a> list</span> * <span><a href="../../EConstr/index.html#type-t">EConstr.t</a> list</span>)</span></span></code></div><div class="spec-doc"><p>Returns the modified arities (the result sort may be replaced by Prop). Should be called with minimized universes.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-error_differing_params" class="anchored"><a href="#val-error_differing_params" class="anchor"></a><code><span><span class="keyword">val</span> error_differing_params : <span>kind:string <span class="arrow">&#45;&gt;</span></span> <span><span>(<a href="../../Names/index.html#type-lident">Names.lident</a> * <a href="../../Vernacexpr/index.html#type-inductive_params_expr">Vernacexpr.inductive_params_expr</a>)</span> <span class="arrow">&#45;&gt;</span></span> <span><span>(<a href="../../Names/index.html#type-lident">Names.lident</a> * <a href="../../Vernacexpr/index.html#type-inductive_params_expr">Vernacexpr.inductive_params_expr</a>)</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div></div></div></body></html>
diff --git a/master/api/coq-core/ComInductive/index.html b/master/api/coq-core/ComInductive/index.html
@@ -1,5 +1,5 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ComInductive (coq-core.ComInductive)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">coq-core</a> &#x00BB; ComInductive</nav><header class="odoc-preamble"><h1>Module <code><span>ComInductive</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#inductive-and-coinductive-types">Inductive and coinductive types</a></li></ul></nav><div class="odoc-content"><h6 id="inductive-and-coinductive-types"><a href="#inductive-and-coinductive-types" class="anchor"></a>Inductive and coinductive types</h6><div class="odoc-spec"><div class="spec type" id="type-flags" class="anchored"><a href="#type-flags" class="anchor"></a><code><span><span class="keyword">type</span> flags</span><span> = </span><span>{</span></code><table><tr id="type-flags.poly" class="anchored"><td class="def record field"><a href="#type-flags.poly" class="anchor"></a><code><span>poly : bool;</span></code></td></tr><tr id="type-flags.cumulative" class="anchored"><td class="def record field"><a href="#type-flags.cumulative" class="anchor"></a><code><span>cumulative : bool;</span></code></td></tr><tr id="type-flags.template" class="anchored"><td class="def record field"><a href="#type-flags.template" class="anchor"></a><code><span>template : <span>bool option</span>;</span></code></td></tr><tr id="type-flags.auto_prop_lowering" class="anchored"><td class="def record field"><a href="#type-flags.auto_prop_lowering" class="anchor"></a><code><span>auto_prop_lowering : bool;</span></code></td></tr><tr id="type-flags.finite" class="anchored"><td class="def record field"><a href="#type-flags.finite" class="anchor"></a><code><span>finite : <a href="../Declarations/index.html#type-recursivity_kind">Declarations.recursivity_kind</a>;</span></code></td></tr><tr id="type-flags.mode" class="anchored"><td class="def record field"><a href="#type-flags.mode" class="anchor"></a><code><span>mode : <span><span><a href="../Hints/index.html#type-hint_mode">Hints.hint_mode</a> list</span> option</span>;</span></code></td></tr></table><code><span>}</span></code></div></div><p>Entry points for the vernacular commands Inductive and CoInductive</p><div class="odoc-spec"><div class="spec type" id="type-uniform_inductive_flag" class="anchored"><a href="#type-uniform_inductive_flag" class="anchor"></a><code><span><span class="keyword">type</span> uniform_inductive_flag</span><span> = </span></code><table><tr id="type-uniform_inductive_flag.UniformParameters" class="anchored"><td class="def variant constructor"><a href="#type-uniform_inductive_flag.UniformParameters" class="anchor"></a><code><span>| </span><span><span class="constructor">UniformParameters</span></span></code></td></tr><tr id="type-uniform_inductive_flag.NonUniformParameters" class="anchored"><td class="def variant constructor"><a href="#type-uniform_inductive_flag.NonUniformParameters" class="anchor"></a><code><span>| </span><span><span class="constructor">NonUniformParameters</span></span></code></td></tr></table></div></div><div class="odoc-spec"><div class="spec value" id="val-do_mutual_inductive" class="anchored"><a href="#val-do_mutual_inductive" class="anchor"></a><code><span><span class="keyword">val</span> do_mutual_inductive : <span>flags:<a href="#type-flags">flags</a> <span class="arrow">&#45;&gt;</span></span> <span>?typing_flags:<a href="../Declarations/index.html#type-typing_flags">Declarations.typing_flags</a> <span class="arrow">&#45;&gt;</span></span>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ComInductive (coq-core.ComInductive)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">coq-core</a> &#x00BB; ComInductive</nav><header class="odoc-preamble"><h1>Module <code><span>ComInductive</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#inductive-and-coinductive-types">Inductive and coinductive types</a></li></ul></nav><div class="odoc-content"><h6 id="inductive-and-coinductive-types"><a href="#inductive-and-coinductive-types" class="anchor"></a>Inductive and coinductive types</h6><div class="odoc-spec"><div class="spec type" id="type-flags" class="anchored"><a href="#type-flags" class="anchor"></a><code><span><span class="keyword">type</span> flags</span><span> = </span><span>{</span></code><table><tr id="type-flags.poly" class="anchored"><td class="def record field"><a href="#type-flags.poly" class="anchor"></a><code><span>poly : bool;</span></code></td></tr><tr id="type-flags.cumulative" class="anchored"><td class="def record field"><a href="#type-flags.cumulative" class="anchor"></a><code><span>cumulative : bool;</span></code></td></tr><tr id="type-flags.template" class="anchored"><td class="def record field"><a href="#type-flags.template" class="anchor"></a><code><span>template : <span>bool option</span>;</span></code></td></tr><tr id="type-flags.finite" class="anchored"><td class="def record field"><a href="#type-flags.finite" class="anchor"></a><code><span>finite : <a href="../Declarations/index.html#type-recursivity_kind">Declarations.recursivity_kind</a>;</span></code></td></tr><tr id="type-flags.mode" class="anchored"><td class="def record field"><a href="#type-flags.mode" class="anchor"></a><code><span>mode : <span><span><a href="../Hints/index.html#type-hint_mode">Hints.hint_mode</a> list</span> option</span>;</span></code></td></tr></table><code><span>}</span></code></div></div><p>Entry points for the vernacular commands Inductive and CoInductive</p><div class="odoc-spec"><div class="spec type" id="type-uniform_inductive_flag" class="anchored"><a href="#type-uniform_inductive_flag" class="anchor"></a><code><span><span class="keyword">type</span> uniform_inductive_flag</span><span> = </span></code><table><tr id="type-uniform_inductive_flag.UniformParameters" class="anchored"><td class="def variant constructor"><a href="#type-uniform_inductive_flag.UniformParameters" class="anchor"></a><code><span>| </span><span><span class="constructor">UniformParameters</span></span></code></td></tr><tr id="type-uniform_inductive_flag.NonUniformParameters" class="anchored"><td class="def variant constructor"><a href="#type-uniform_inductive_flag.NonUniformParameters" class="anchor"></a><code><span>| </span><span><span class="constructor">NonUniformParameters</span></span></code></td></tr></table></div></div><div class="odoc-spec"><div class="spec value" id="val-do_mutual_inductive" class="anchored"><a href="#val-do_mutual_inductive" class="anchor"></a><code><span><span class="keyword">val</span> do_mutual_inductive : <span>flags:<a href="#type-flags">flags</a> <span class="arrow">&#45;&gt;</span></span> <span>?typing_flags:<a href="../Declarations/index.html#type-typing_flags">Declarations.typing_flags</a> <span class="arrow">&#45;&gt;</span></span>
 <span><span><a href="../Constrexpr/index.html#type-cumul_univ_decl_expr">Constrexpr.cumul_univ_decl_expr</a> option</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>(<a href="../Vernacexpr/index.html#type-one_inductive_expr">Vernacexpr.one_inductive_expr</a> * <span><a href="../Vernacexpr/index.html#type-notation_declaration">Vernacexpr.notation_declaration</a> list</span>)</span> list</span> <span class="arrow">&#45;&gt;</span></span> <span>private_ind:bool <span class="arrow">&#45;&gt;</span></span> <span>uniform:<a href="#type-uniform_inductive_flag">uniform_inductive_flag</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><p>User-interface API</p><p>Prepare a &quot;match&quot; template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables. <code>Not_found</code> is raised if the given string isn't the qualid of a known inductive type.</p><div class="odoc-spec"><div class="spec value" id="val-make_cases" class="anchored"><a href="#val-make_cases" class="anchor"></a><code><span><span class="keyword">val</span> make_cases : <span><a href="../Names/index.html#type-inductive">Names.inductive</a> <span class="arrow">&#45;&gt;</span></span> <span><span>string list</span> list</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Mind_decl" class="anchored"><a href="#module-Mind_decl" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Mind_decl/index.html">Mind_decl</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-interp_mutual_inductive" class="anchored"><a href="#val-interp_mutual_inductive" class="anchor"></a><code><span><span class="keyword">val</span> interp_mutual_inductive : <span>env:<a href="../Environ/index.html#type-env">Environ.env</a> <span class="arrow">&#45;&gt;</span></span> <span>flags:<a href="#type-flags">flags</a> <span class="arrow">&#45;&gt;</span></span> <span>?typing_flags:<a href="../Declarations/index.html#type-typing_flags">Declarations.typing_flags</a> <span class="arrow">&#45;&gt;</span></span>
 <span><span><a href="../Constrexpr/index.html#type-cumul_univ_decl_expr">Constrexpr.cumul_univ_decl_expr</a> option</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>(<a href="../Vernacexpr/index.html#type-one_inductive_expr">Vernacexpr.one_inductive_expr</a> * <span><a href="../Vernacexpr/index.html#type-notation_declaration">Vernacexpr.notation_declaration</a> list</span>)</span> list</span> <span class="arrow">&#45;&gt;</span></span> <span>private_ind:bool <span class="arrow">&#45;&gt;</span></span> <span>uniform:<a href="#type-uniform_inductive_flag">uniform_inductive_flag</a> <span class="arrow">&#45;&gt;</span></span> <a href="Mind_decl/index.html#type-t">Mind_decl.t</a></span></code></div><div class="spec-doc"><p>elaborates an inductive declaration (the first half of do_mutual_inductive)</p></div></div><div class="odoc-spec"><div class="spec type" id="type-syntax_allows_template_poly" class="anchored"><a href="#type-syntax_allows_template_poly" class="anchor"></a><code><span><span class="keyword">type</span> syntax_allows_template_poly</span><span> = </span></code><table><tr id="type-syntax_allows_template_poly.SyntaxAllowsTemplatePoly" class="anchored"><td class="def variant constructor"><a href="#type-syntax_allows_template_poly.SyntaxAllowsTemplatePoly" class="anchor"></a><code><span>| </span><span><span class="constructor">SyntaxAllowsTemplatePoly</span></span></code></td></tr><tr id="type-syntax_allows_template_poly.SyntaxNoTemplatePoly" class="anchored"><td class="def variant constructor"><a href="#type-syntax_allows_template_poly.SyntaxNoTemplatePoly" class="anchor"></a><code><span>| </span><span><span class="constructor">SyntaxNoTemplatePoly</span></span></code></td></tr></table></div></div><div class="odoc-spec"><div class="spec value" id="val-interp_mutual_inductive_constr" class="anchored"><a href="#val-interp_mutual_inductive_constr" class="anchor"></a><code><span><span class="keyword">val</span> interp_mutual_inductive_constr : <span>sigma:<a href="../Evd/index.html#type-evar_map">Evd.evar_map</a> <span class="arrow">&#45;&gt;</span></span> <span>flags:<a href="#type-flags">flags</a> <span class="arrow">&#45;&gt;</span></span> <span>udecl:<a href="../UState/index.html#type-universe_decl">UState.universe_decl</a> <span class="arrow">&#45;&gt;</span></span> <span>variances:<a href="../Entries/index.html#type-variance_entry">Entries.variance_entry</a> <span class="arrow">&#45;&gt;</span></span>
 <span>ctx_params:<a href="../EConstr/index.html#type-rel_context">EConstr.rel_context</a> <span class="arrow">&#45;&gt;</span></span> <span>indnames:<span><a href="../Names/Id/index.html#type-t">Names.Id.t</a> list</span> <span class="arrow">&#45;&gt;</span></span> <span>arities_explicit:<span>bool list</span> <span class="arrow">&#45;&gt;</span></span> <span>arities:<span><a href="../EConstr/index.html#type-t">EConstr.t</a> list</span> <span class="arrow">&#45;&gt;</span></span>

diff --git a/master/refman/.doctrees/addendum/extraction.doctree b/master/refman/.doctrees/addendum/extraction.doctree
diff --git a/master/refman/.doctrees/addendum/generalized-rewriting.doctree b/master/refman/.doctrees/addendum/generalized-rewriting.doctree
diff --git a/master/refman/.doctrees/addendum/implicit-coercions.doctree b/master/refman/.doctrees/addendum/implicit-coercions.doctree
diff --git a/master/refman/.doctrees/addendum/micromega.doctree b/master/refman/.doctrees/addendum/micromega.doctree
diff --git a/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree b/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree
diff --git a/master/refman/.doctrees/addendum/program.doctree b/master/refman/.doctrees/addendum/program.doctree
diff --git a/master/refman/.doctrees/addendum/rewrite-rules.doctree b/master/refman/.doctrees/addendum/rewrite-rules.doctree
diff --git a/master/refman/.doctrees/addendum/ring.doctree b/master/refman/.doctrees/addendum/ring.doctree
diff --git a/master/refman/.doctrees/addendum/sprop.doctree b/master/refman/.doctrees/addendum/sprop.doctree
diff --git a/master/refman/.doctrees/addendum/type-classes.doctree b/master/refman/.doctrees/addendum/type-classes.doctree
diff --git a/master/refman/.doctrees/addendum/universe-polymorphism.doctree b/master/refman/.doctrees/addendum/universe-polymorphism.doctree
diff --git a/master/refman/.doctrees/changes.doctree b/master/refman/.doctrees/changes.doctree
diff --git a/master/refman/.doctrees/environment.pickle b/master/refman/.doctrees/environment.pickle
diff --git a/master/refman/.doctrees/language/cic.doctree b/master/refman/.doctrees/language/cic.doctree
diff --git a/master/refman/.doctrees/language/coq-library.doctree b/master/refman/.doctrees/language/coq-library.doctree
diff --git a/master/refman/.doctrees/language/core/assumptions.doctree b/master/refman/.doctrees/language/core/assumptions.doctree
diff --git a/master/refman/.doctrees/language/core/basic.doctree b/master/refman/.doctrees/language/core/basic.doctree
diff --git a/master/refman/.doctrees/language/core/coinductive.doctree b/master/refman/.doctrees/language/core/coinductive.doctree
diff --git a/master/refman/.doctrees/language/core/conversion.doctree b/master/refman/.doctrees/language/core/conversion.doctree
diff --git a/master/refman/.doctrees/language/core/inductive.doctree b/master/refman/.doctrees/language/core/inductive.doctree
diff --git a/master/refman/.doctrees/language/core/modules.doctree b/master/refman/.doctrees/language/core/modules.doctree
diff --git a/master/refman/.doctrees/language/core/primitive.doctree b/master/refman/.doctrees/language/core/primitive.doctree
diff --git a/master/refman/.doctrees/language/core/records.doctree b/master/refman/.doctrees/language/core/records.doctree
diff --git a/master/refman/.doctrees/language/core/sections.doctree b/master/refman/.doctrees/language/core/sections.doctree
diff --git a/master/refman/.doctrees/language/core/variants.doctree b/master/refman/.doctrees/language/core/variants.doctree
diff --git a/master/refman/.doctrees/language/extensions/arguments-command.doctree b/master/refman/.doctrees/language/extensions/arguments-command.doctree
diff --git a/master/refman/.doctrees/language/extensions/canonical.doctree b/master/refman/.doctrees/language/extensions/canonical.doctree
diff --git a/master/refman/.doctrees/language/extensions/evars.doctree b/master/refman/.doctrees/language/extensions/evars.doctree
diff --git a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree
diff --git a/master/refman/.doctrees/language/extensions/match.doctree b/master/refman/.doctrees/language/extensions/match.doctree
diff --git a/master/refman/.doctrees/practical-tools/coq-commands.doctree b/master/refman/.doctrees/practical-tools/coq-commands.doctree
diff --git a/master/refman/.doctrees/practical-tools/coqide.doctree b/master/refman/.doctrees/practical-tools/coqide.doctree
diff --git a/master/refman/.doctrees/proof-engine/ltac.doctree b/master/refman/.doctrees/proof-engine/ltac.doctree
diff --git a/master/refman/.doctrees/proof-engine/ltac2.doctree b/master/refman/.doctrees/proof-engine/ltac2.doctree
diff --git a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree
diff --git a/master/refman/.doctrees/proof-engine/tactics.doctree b/master/refman/.doctrees/proof-engine/tactics.doctree
diff --git a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree b/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree
diff --git a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree
diff --git a/master/refman/.doctrees/using/libraries/funind.doctree b/master/refman/.doctrees/using/libraries/funind.doctree
diff --git a/master/refman/.doctrees/using/libraries/writing.doctree b/master/refman/.doctrees/using/libraries/writing.doctree
diff --git a/master/refman/_sources/changes.rst.txt b/master/refman/_sources/changes.rst.txt
@@ -524,9 +524,8 @@ Ltac2 language
   (`#18988 <https://github.com/coq/coq/pull/18988>`_,
   by Gaëtan Gilbert).
 - **Added:**
-  :flag:`Automatic Proposition Inductives`, :flag:`Dependent Proposition Eliminators` and
-  :warn:`warning when automatically lowering an inductive declared with Type to Prop
-  <automatic-prop-lowering>`
+  flag `Automatic Proposition Inductives`, :flag:`Dependent Proposition Eliminators` and
+  warning `automatic-prop-lowering`
   (`#18989 <https://github.com/coq/coq/pull/18989>`_,
   by Gaëtan Gilbert).
 - **Added:**