aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/README.rst9
-rw-r--r--doc/sphinx/README.template.rst7
-rw-r--r--doc/sphinx/_static/coqnotations.sty29
-rw-r--r--doc/sphinx/_static/notations.css37
-rw-r--r--doc/sphinx/addendum/extraction.rst2
-rw-r--r--doc/sphinx/addendum/generalized-rewriting.rst25
-rw-r--r--doc/sphinx/addendum/program.rst2
-rw-r--r--doc/sphinx/addendum/type-classes.rst39
-rw-r--r--doc/sphinx/changes.rst11
-rw-r--r--doc/sphinx/language/gallina-extensions.rst24
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst26
-rw-r--r--doc/sphinx/proof-engine/ltac.rst28
-rw-r--r--doc/sphinx/proof-engine/ltac2.rst10
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst12
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst22
-rw-r--r--doc/sphinx/proof-engine/tactics.rst31
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst32
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst27
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst31
19 files changed, 235 insertions, 169 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 881f7a310d..b20669c7f1 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
``{*, …}``, ``{+, …}``
an optional or mandatory repeatable block, with repetitions separated by commas
-``%|``, ``%{``, …
- an escaped character (rendered without the leading ``%``)
+``{| … | … | … }``
+ an alternative, indicating than one of multiple constructs can be used
+
+``%{``, ``%}``, ``%|``
+ an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
..
FIXME document the new subscript support
@@ -148,7 +151,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
Example::
.. prodn:: term += let: @pattern := @term in @term
- .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+ .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values.
Example::
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 78803a927f..2093765608 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
``{*, …}``, ``{+, …}``
an optional or mandatory repeatable block, with repetitions separated by commas
-``%|``, ``%{``, …
- an escaped character (rendered without the leading ``%``)
+``{| … | … | … }``
+ an alternative, indicating than one of multiple constructs can be used
+
+``%{``, ``%}``, ``%|``
+ an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
..
FIXME document the new subscript support
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 75eac1f724..3548b8754c 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -18,6 +18,9 @@
\newlength{\nscriptsize}
\setlength{\nscriptsize}{0.8em}
+\newlength{\nboxsep}
+\setlength{\nboxsep}{2pt}
+
\newcommand*{\scriptsmallsquarebox}[1]{%
% Force width
\makebox[\nscriptsize]{%
@@ -31,7 +34,8 @@
\newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}}
\newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}}
\newcommand*{\nnotation}[1]{#1}
-\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}}
+\newcommand*{\nbox}[1]{\adjustbox{cfbox=nbordercolor 0.5pt \nboxsep,bgcolor=nbgcolor}{#1}}
+\newcommand*{\nrepeat}[1]{\text{\nbox{#1\hspace{.5\nscriptsize}}}}
\newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/
\newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}}
@@ -42,9 +46,32 @@
}
% </magic>
+% https://tex.stackexchange.com/questions/490262/
+\def\naltsep{}
+\newsavebox{\nsavedalt}
+\newlength{\naltvruleht}
+\newlength{\naltvruledp}
+\def\naltvrule{\smash{\vrule height\naltvruleht depth\naltvruledp}}
+\newcommand{\nalternative}[2]{%
+ % First measure the contents of the box without the bar
+ \bgroup%
+ \def\naltsep{}%
+ \savebox{\nsavedalt}{#1}%
+ \setlength{\naltvruleht}{\ht\nsavedalt}%
+ \setlength{\naltvruledp}{\dp\nsavedalt}%
+ \addtolength{\naltvruleht}{#2}%
+ \addtolength{\naltvruledp}{#2}%
+ % Then redraw it with the bar
+ \def\naltsep{\naltvrule}%
+ #1\egroup}
+
\newcssclass{notation-sup}{\nsup{#1}}
\newcssclass{notation-sub}{\nsub{#1}}
\newcssclass{notation}{\nnotation{#1}}
\newcssclass{repeat}{\nrepeat{#1}}
\newcssclass{repeat-wrapper}{\nwrapper{#1}}
\newcssclass{hole}{\nhole{#1}}
+\newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}}
+\newcssclass{alternative-block}{#1}
+\newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}}
+\newcssclass{alternative-separator}{\quad\naltsep{}\quad}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index dcb47d1786..8322ab0137 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -45,15 +45,46 @@
width: 2.2em;
}
-.notation .repeat {
+.notation .repeat, .notation .alternative {
background: #EAEAEA;
border: 1px solid #AAA;
display: inline-block;
- padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
- padding-left: 0.2em;
+ padding: 0 0.2em 0 0.3em;
margin: 0.25em 0;
}
+.notation .repeated-alternative {
+ display: inline-table;
+}
+
+.notation .alternative {
+ display: inline-table;
+ padding: 0 0.2em;
+}
+
+.notation .alternative-block {
+ display: table-cell;
+ padding: 0 0.5em;
+}
+
+.notation .alternative-separator {
+ border-left: 1px solid black; /* Display a thin bar */
+ display: table-cell;
+ width: 0;
+}
+
+.alternative-block:first-child {
+ padding-left: 0;
+}
+
+.alternative-block:last-child {
+ padding-right: 0;
+}
+
+.notation .repeat {
+ padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
+}
+
.notation .repeat-wrapper {
display: inline-block;
position: relative;
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index e93b01f14d..8a895eb515 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,7 +99,7 @@ Extraction Options
Setting the target language
~~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. cmd:: Extraction Language ( OCaml | Haskell | Scheme )
+.. cmd:: Extraction Language {| OCaml | Haskell | Scheme }
:name: Extraction Language
The ability to fix target language is the first and more important
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index b474c51f17..847abb33fc 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,12 +170,12 @@ compatibility constraints.
Adding new relations and morphisms
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident
+.. cmd:: Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
:g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
- The :token:`ident` gives a unique name to the morphism and it is used
+ The final :token:`ident` gives a unique name to the morphism and it is used
by the command to generate fresh names for automatically provided
lemmas used internally.
@@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic
compositions of parametric morphism instances declared with the
following command.
-.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident
+.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident
- This command declares ``f`` as a parametric morphism of signature ``sig``. The
- identifier :token:`ident` gives a unique name to the morphism and it is used as
- the base name of the typeclass instance definition and as the name of
- the lemma that proves the well-definedness of the morphism. The
- parameters of the morphism as well as the signature may refer to the
- context of variables. The command asks the user to prove interactively
- that ``f`` respects the relations identified from the signature.
+ This command declares a parametric morphism :n:`@ident {+ @term__1}` of
+ signature :n:`@term__2`. The final identifier :token:`ident` gives a unique
+ name to the morphism and it is used as the base name of the typeclass
+ instance definition and as the name of the lemma that proves the
+ well-definedness of the morphism. The parameters of the morphism as well as
+ the signature may refer to the context of variables. The command asks the
+ user to prove interactively that the function denoted by the first
+ :token:`ident` respects the relations identified from the signature.
.. example::
@@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities
Notice that the syntax is not completely backward compatible since the
identifier was not required.
-.. cmd:: Add Morphism f : @ident
+.. cmd:: Add Morphism @ident : @ident
:name: Add Morphism
This command is restricted to the declaration of morphisms
@@ -809,7 +810,7 @@ Usage
~~~~~
-.. tacn:: rewrite_strat @s [in @ident]
+.. tacn:: rewrite_strat @s {? in @ident }
:name: rewrite_strat
Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b410833d25..22ddcae584 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved
obligations (e.g. when defining mutually recursive blocks). The
optional tactic is replaced by the default one if not specified.
-.. cmd:: {? Local|Global} Obligation Tactic := @tactic
+.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic
:name: Obligation Tactic
Sets the default obligation solving tactic applied to all obligations
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 77a6ee79cc..65934efaa6 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -311,24 +311,24 @@ Summary of the commands
This command has no effect when used on a typeclass.
-.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
This command is used to declare a typeclass instance named
- :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
- fields ``b1`` to ``bi``, where each field must be a declared field of
- the class. Missing fields must be filled in interactive proof mode.
+ :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
+ fields defined by :token:`field_def`, where each field must be a declared field of
+ the class.
An arbitrary context of :token:`binders` can be put after the name of the
instance and before the colon to declare a parameterized instance. An
optional priority can be declared, 0 being the highest priority as for
- :tacn:`auto` hints. If the priority is not specified, it defaults to the number
+ :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
of non-dependent binders of the instance.
- .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
+ .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term
This syntax is used for declaration of singleton class instances or
- for directly giving an explicit term of type :n:`forall @binders, @class
- @term__1 … @term__n`. One need not even mention the unique field name for
+ for directly giving an explicit term of type :n:`forall @binders, @term__0
+ {+ @term}`. One need not even mention the unique field name for
singleton classes.
.. cmdv:: Global Instance
@@ -356,11 +356,11 @@ Summary of the commands
Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
few other commands related to typeclasses.
-.. cmd:: Existing Instance {+ @ident} [| priority]
+.. cmd:: Existing Instance {+ @ident} {? | @num}
This command adds an arbitrary list of constants whose type ends with
an applied typeclass to the instance database with an optional
- priority. It can be used for redeclaring instances at the end of
+ priority :token:`num`. It can be used for redeclaring instances at the end of
sections, or declaring structure projections as instances. This is
equivalent to ``Hint Resolve ident : typeclass_instances``, except it
registers instances for :cmd:`Print Instances`.
@@ -408,7 +408,7 @@ few other commands related to typeclasses.
+ When considering local hypotheses, we use the union of all the modes
declared in the given databases.
- .. cmdv:: typeclasses eauto @num
+ .. tacv:: typeclasses eauto @num
.. warning::
The semantics for the limit :n:`@num`
@@ -417,7 +417,7 @@ few other commands related to typeclasses.
counted, which might result in larger limits being necessary when
searching with ``typeclasses eauto`` than with :tacn:`auto`.
- .. cmdv:: typeclasses eauto with {+ @ident}
+ .. tacv:: typeclasses eauto with {+ @ident}
This variant runs resolution with the given hint databases. It treats
typeclass subgoals the same as other subgoals (no shelving of
@@ -563,23 +563,10 @@ Settings
of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this
option to 0 turns that option off.
-.. flag:: Refine Instance Mode
-
- .. deprecated:: 8.10
-
- This flag allows to switch the behavior of instance declarations made through
- the Instance command.
-
- + When it is off (the default), they fail with an error instead.
-
- + When it is on, instances that have unsolved holes in
- their proof-term silently open the proof mode with the remaining
- obligations to prove.
-
Typeclasses eauto `:=`
~~~~~~~~~~~~~~~~~~~~~~
-.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num
+.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num
:name: Typeclasses eauto
This command allows more global customization of the typeclass
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index cca3b2e06b..cc2c43e7dd 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -486,10 +486,9 @@ Other changes in 8.10+beta1
- :cmd:`Declare Instance` now requires an instance name.
- The flag :flag:`Refine Instance Mode` has been turned off by default,
- meaning that :cmd:`Instance` no longer opens a proof when a body is
- provided. The flag has been deprecated and will be removed in the next
- version.
+ The flag `Refine Instance Mode` has been turned off by default, meaning that
+ :cmd:`Instance` no longer opens a proof when a body is provided. The flag
+ has been deprecated and will be removed in the next version.
(`#9270 <https://github.com/coq/coq/pull/9270>`_,
and `#9825 <https://github.com/coq/coq/pull/9825>`_,
@@ -498,7 +497,7 @@ Other changes in 8.10+beta1
- Command :cmd:`Instance`, when no body is provided, now always opens
a proof. This is a breaking change, as instance of :n:`Instance
@ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will
- have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.`
+ have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.`
or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`
(`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès).
@@ -3940,7 +3939,7 @@ Vernacular commands
Equality Schemes", this replaces deprecated option "Equality Scheme").
- Made support for automatic generation of case analysis schemes available
to user (governed by option "Set Case Analysis Schemes").
-- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to
+- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to
declare which identifiers are generalizable in `` `{} `` and `` `() `` binders.
- New command "Print Opaque Dependencies" to display opaque constants in
addition to all variables, parameters or axioms a theorem or
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ba766c8c3d..5e214f6f7f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor
.. productionlist::
record_term : {| [`field_def` ; … ; `field_def`] |}
- field_def : name [binders] := `record_term`
+ field_def : `ident` [`binders`] := `term`
Alternatively, the following syntax allows creating objects by using named fields, as
shown in this grammar. The fields do not have to be in any particular order, nor do they have
@@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions.
Links :token:`type` to each :token:`ident`.
- .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
+ .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
Declare one or more variables with various types.
- .. cmdv:: Variables {+ ( {+ @ident } : @type) }
- Hypothesis {+ ( {+ @ident } : @type) }
- Hypotheses {+ ( {+ @ident } : @type) }
+ .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+ Hypothesis {+ ( {+ @ident } : @type) }
+ Hypotheses {+ ( {+ @ident } : @type) }
:name: Variables; Hypothesis; Hypotheses
- These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
+ These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
.. cmd:: Let @ident := @term
@@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any
:token:`module_binding`. The output module type
is verified against each :token:`module_type`.
-.. cmdv:: Module [ Import | Export ]
+.. cmdv:: Module {| Import | Export }
Behaves like :cmd:`Module`, but automatically imports or exports the module.
@@ -1648,7 +1648,7 @@ Declaring Implicit Arguments
-.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
:name: Arguments (implicits)
This command is used to set implicit arguments *a posteriori*,
@@ -1665,20 +1665,20 @@ Declaring Implicit Arguments
This command clears implicit arguments.
-.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
This command is used to recompute the implicit arguments of
:token:`qualid` after ending of the current section if any, enforcing the
implicit arguments known from inside the section to be the ones
declared by the command.
-.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
When in a module, tell not to activate the
implicit arguments of :token:`qualid` declared by this command to contexts that
require the module.
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } }
+.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } }
For names of constants, inductive types,
constructors, lemmas which can only be applied to a fixed number of
@@ -2167,7 +2167,7 @@ that specify which variables should be generalizable.
Disable implicit generalization entirely. This is the default behavior.
-.. cmd:: Generalizable (Variable | Variables) {+ @ident }
+.. cmd:: Generalizable {| Variable | Variables } {+ @ident }
Allow generalization of the given identifiers only. Calling this command multiple times
adds to the allowed identifiers.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 5a1af9f9fa..8acbcbec8f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -616,34 +616,34 @@ has type :token:`type`.
Adds several parameters with specification :token:`type`.
- .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
+ .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
Adds blocks of parameters with different specifications.
- .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
+ .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
:name: Local Parameter
Such parameters are never made accessible through their unqualified name by
:cmd:`Import` and its variants. You have to explicitly give their fully
qualified name to refer to them.
- .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
- {? Local } Axiom {+ ( {+ @ident } : @type ) }
- {? Local } Axioms {+ ( {+ @ident } : @type ) }
- {? Local } Conjecture {+ ( {+ @ident } : @type ) }
- {? Local } Conjectures {+ ( {+ @ident } : @type ) }
+ .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
+ {? Local } Axiom {+ ( {+ @ident } : @type ) }
+ {? Local } Axioms {+ ( {+ @ident } : @type ) }
+ {? Local } Conjecture {+ ( {+ @ident } : @type ) }
+ {? Local } Conjectures {+ ( {+ @ident } : @type ) }
:name: Parameters; Axiom; Axioms; Conjecture; Conjectures
- These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
+ These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
- .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
- Variables {+ ( {+ @ident } : @type ) }
- Hypothesis {+ ( {+ @ident } : @type ) }
- Hypotheses {+ ( {+ @ident } : @type ) }
+ .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
+ Variables {+ ( {+ @ident } : @type ) }
+ Hypothesis {+ ( {+ @ident } : @type ) }
+ Hypotheses {+ ( {+ @ident } : @type ) }
:name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
Outside of any section, these variants are synonyms of
- :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+ :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
For their meaning inside a section, see :cmd:`Variable` in
:ref:`section-mechanism`.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index a7eb7c2319..bbd7e0ba3d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -360,7 +360,7 @@ Detecting progress
We can check if a tactic made progress with:
-.. tacn:: progress expr
+.. tacn:: progress @expr
:name: progress
:n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v``
@@ -555,7 +555,7 @@ Identity
The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but
it appears in the proof script.
-.. tacn:: idtac {* message_token}
+.. tacn:: idtac {* @message_token}
:name: idtac
This prints the given tokens. Strings and integers are printed
@@ -684,7 +684,7 @@ Timing a tactic that evaluates to a term
Tactic expressions that produce terms can be timed with the experimental
tactic
-.. tacn:: time_constr expr
+.. tacn:: time_constr @expr
:name: time_constr
which evaluates :n:`@expr ()` and displays the time the tactic expression
@@ -880,7 +880,7 @@ We can perform pattern matching on goals using the following expression:
.. we should provide the full grammar here
-.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
:name: match goal
If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is
@@ -918,7 +918,7 @@ We can perform pattern matching on goals using the following expression:
first), but it possible to reverse this order (oldest first)
with the :n:`match reverse goal with` variant.
- .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+ .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics
to backtrack into a right-hand side tactic which has backtracking points
@@ -929,7 +929,7 @@ We can perform pattern matching on goals using the following expression:
The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for
:n:`once multimatch [reverse] goal …`.
- .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+ .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
Using lazymatch instead of match will perform the same pattern matching
procedure but will commit to the first matching branch with the first
@@ -1135,33 +1135,33 @@ Defining |Ltac| functions
Basically, |Ltac| toplevel definitions are made as follows:
-.. cmd:: Ltac @ident {* @ident} := @expr
+.. cmd:: {? Local} Ltac @ident {* @ident} := @expr
+ :name: Ltac
This defines a new |Ltac| function that can be used in any tactic
script or new |Ltac| toplevel definition.
+ If preceded by the keyword ``Local``, the tactic definition will not be
+ exported outside the current module.
+
.. note::
The preceding definition can equivalently be written:
:n:`Ltac @ident := fun {+ @ident} => @expr`
- Recursive and mutual recursive function definitions are also possible
- with the syntax:
-
.. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr
- It is also possible to *redefine* an existing user-defined tactic using the syntax:
+ This syntax allows recursive and mutual recursive function definitions.
.. cmdv:: Ltac @qualid {* @ident} ::= @expr
+ This syntax *redefines* an existing user-defined tactic.
+
A previous definition of qualid must exist in the environment. The new
definition will always be used instead of the old one and it goes across
module boundaries.
- If preceded by the keyword Local the tactic definition will not be
- exported outside the current module.
-
Printing |Ltac| tactics
~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 6e33862b39..aa603fc966 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -668,7 +668,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression
at parsing time. Scopes are described using a form of S-expression.
.. prodn::
- ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope})
+ ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) }
A few scopes contain antiquotation features. For sake of uniformity, all
antiquotations are introduced by the syntax :n:`$@lident`.
@@ -751,7 +751,7 @@ Notations
The Ltac2 parser can be extended by syntactic notations.
-.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term
+.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term
:name: Ltac2 Notation
A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
@@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions.
Debug
-----
-.. opt:: Ltac2 Backtrace
+.. flag:: Ltac2 Backtrace
- When this option is set, toplevel failures will be printed with a backtrace.
+ When this flag is set, toplevel failures will be printed with a backtrace.
Compatibility layer with Ltac1
------------------------------
@@ -966,7 +966,7 @@ errors produced by the typechecker.
In Ltac expressions
+++++++++++++++++++
-.. exn:: Unbound ( value | constructor ) X
+.. exn:: Unbound {| value | constructor } X
* if `X` is meant to be a term from the current stactic environment, replace
the problematic use by `'X`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 16b158c397..4a2f9c0db3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -322,7 +322,7 @@ Navigation in the proof tree
.. index:: {
}
-.. cmd:: %{ %| %}
+.. cmd:: {| %{ | %} }
The command ``{`` (without a terminating period) focuses on the first
goal, much like :cmd:`Focus` does, however, the subproof can only be
@@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
nesting levels provided they are delimited by these. Bullets are made of
repeated ``-``, ``+`` or ``*`` symbols:
-.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * }
+.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } }
Note again that when a focused goal is proved a message is displayed
together with a suggestion about the right bullet or ``}`` to unfocus it
@@ -492,7 +492,7 @@ The following example script illustrates all these features:
Set Bullet Behavior
```````````````````
-.. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %)
+.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
:name: Bullet Behavior
This option controls the bullet behavior and can take two possible values:
@@ -544,9 +544,9 @@ Requesting information
``<Your Tactic Text here>``.
- .. deprecated:: 8.10
+ .. deprecated:: 8.10
- Please use a text editor.
+ Please use a text editor.
.. cmdv:: Show Proof
:name: Show Proof
@@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE:
How to enable diffs
```````````````````
-.. opt:: Diffs %( "on" %| "off" %| "removed" %)
+.. opt:: Diffs {| "on" | "off" | "removed" }
:name: Diffs
The “on” setting highlights added tokens in green, while the “removed” setting
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4e40df6f94..75e019592f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -617,7 +617,7 @@ Abbreviations
selected occurrences of a term.
.. prodn::
- occ_switch ::= { {? + %| - } {* @num } }
+ occ_switch ::= { {? {| + | - } } {* @num } }
where:
@@ -2273,7 +2273,7 @@ to the others.
Iteration
~~~~~~~~~
-.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] )
+.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] }
:name: do (ssreflect)
This tactical offers an accurate control on the repetition of tactics.
@@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal.
There are four kinds of multipliers:
.. prodn::
- mult ::= @num ! %| ! %| @num ? %| ?
+ mult ::= {| @num ! | ! | @num ? | ? }
Their meaning is:
@@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic:
An alternative use of the ``have`` tactic is to provide the explicit proof
term for the intermediate lemma, using tactics of the form:
-.. tacv:: have {? @ident } := term
+.. tacv:: have {? @ident } := @term
This tactic creates a new assumption of type the type of :token:`term`.
If the
@@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single
|SSR| searching tool
--------------------
-.. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } }
+.. cmd:: Search {? @pattern } {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } }
:name: Search (ssreflect)
This is the |SSR| extension of the Search command. :token:`qualid` is the
@@ -5686,7 +5686,7 @@ respectively.
local cofix definition
-.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %)
+.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) }
abbreviation (see :ref:`abbreviations_ssr`)
@@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr`
localization see :ref:`localization_ssr`
-.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %)
+.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] }
iteration see :ref:`iteration_ssr`
-.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %)
+.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] }
selector see :ref:`selectors_ssr`
-.. prodn:: tactic += @tactic ; %( first %| last %) {? @num }
+.. prodn:: tactic += @tactic ; {| first | last } {? @num }
rotation see :ref:`selectors_ssr`
-.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %)
+.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] }
closing see :ref:`terminators_ssr`
Commands
~~~~~~~~
-.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num }
+.. cmd:: Hint View for {| move | apply } / @ident {? | @num }
view hint declaration (see :ref:`declaring_new_hints_ssr`)
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index c728b925ac..4e47621938 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``,
and ``in`` clauses.
-.. tacn:: case term
+.. tacn:: case @term
:name: case
The tactic :n:`case` is a more basic tactic to perform case analysis without
@@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
:n:`induction @ident; induction @ident` (or
:n:`induction @ident ; destruct @ident` depending on the exact needs).
-.. tacv:: double induction num1 num2
+.. tacv:: double induction @num__1 @num__2
This tactic is deprecated and should be replaced by
:n:`induction num1; induction num3` where :n:`num3` is the result
@@ -2271,11 +2271,11 @@ and an explanation of the underlying technique.
:undocumented:
.. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern}
- injection @num as {+ simple_intropattern}
- injection as {+ simple_intropattern}
- einjection @term {? with @bindings_list} as {+ simple_intropattern}
- einjection @num as {+ simple_intropattern}
- einjection as {+ simple_intropattern}
+ injection @num as {+ @simple_intropattern}
+ injection as {+ @simple_intropattern}
+ einjection @term {? with @bindings_list} as {+ @simple_intropattern}
+ einjection @num as {+ @simple_intropattern}
+ einjection as {+ @simple_intropattern}
These variants apply :n:`intros {+ @simple_intropattern}` after the call to
:tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
@@ -2637,7 +2637,7 @@ and an explanation of the underlying technique.
is correct at some time of the interactive development of a proof, use
the command ``Guarded`` (see Section :ref:`requestinginformation`).
-.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)}
+.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)}
This starts a proof by mutual induction. The statements to be simultaneously
proved are respectively :g:`forall binder ... binder, type`.
@@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
discrimination network to relax or constrain it in the case of discriminated
databases.
- .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident
- Hint Constants %( Transparent %| Opaque %) : @ident
+ .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident
+ Hint Constants {| Transparent | Opaque } : @ident
:name: Hint Variables; Hint Constants
This sets the transparency flag used during unification of
@@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
semantics of :n:`Hint Cut @regexp` is to set the cut expression
to :n:`c | regexp`, the initial cut expression being `emp`.
- .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident
+ .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident
:name: Hint Mode
This sets an optional mode of use of the identifier :n:`@qualid`. When
@@ -4016,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior
option which accepts three flags allowing for a fine-grained handling of
non-imported hints.
-.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %)
+.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" }
:name: Loose Hint Behavior
This option accepts three values, which control the behavior of hints w.r.t.
@@ -4048,7 +4048,7 @@ Setting implicit automation tactics
.. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`.
- .. cmdv:: Proof with tactic using {+ @ident}
+ .. cmdv:: Proof with @tactic using {+ @ident}
Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
@@ -4400,6 +4400,11 @@ Equality
This tactic applies to a goal that has the form :g:`t=u` and transforms it
into the two subgoals :n:`t=@term` and :n:`@term=u`.
+ .. tacv:: etransitivity
+
+ This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of
+ a concrete :token:`term`.
+
Equality and inductive sets
---------------------------
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e207a072cc..26dc4e02cf 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,13 +91,13 @@ and tables:
Flags, options and tables are identified by a series of identifiers, each with an initial
capital letter.
-.. cmd:: {? Local | Global | Export } Set @flag
+.. cmd:: {? {| Local | Global | Export } } Set @flag
:name: Set
Sets :token:`flag` on. Scoping qualifiers are
described :ref:`here <set_unset_scope_qualifiers>`.
-.. cmd:: {? Local | Global | Export } Unset @flag
+.. cmd:: {? {| Local | Global | Export } } Unset @flag
:name: Unset
Sets :token:`flag` off. Scoping qualifiers are
@@ -108,13 +108,13 @@ capital letter.
Prints the current value of :token:`flag`.
-.. cmd:: {? Local | Global | Export } Set @option ( @num | @string )
+.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string }
:name: Set @option
Sets :token:`option` to the specified value. Scoping qualifiers are
described :ref:`here <set_unset_scope_qualifiers>`.
-.. cmd:: {? Local | Global | Export } Unset @option
+.. cmd:: {? {| Local | Global | Export } } Unset @option
:name: Unset @option
Sets :token:`option` to its default value. Scoping qualifiers are
@@ -129,17 +129,17 @@ capital letter.
Prints the current value of all flags and options, and the names of all tables.
-.. cmd:: Add @table ( @string | @qualid )
+.. cmd:: Add @table {| @string | @qualid }
:name: Add @table
Adds the specified value to :token:`table`.
-.. cmd:: Remove @table ( @string | @qualid )
+.. cmd:: Remove @table {| @string | @qualid }
:name: Remove @table
Removes the specified value from :token:`table`.
-.. cmd:: Test @table for ( @string | @qualid )
+.. cmd:: Test @table for {| @string | @qualid }
:name: Test @table for
Reports whether :token:`table` contains the specified value.
@@ -162,7 +162,7 @@ capital letter.
Scope qualifiers for :cmd:`Set` and :cmd:`Unset`
`````````````````````````````````````````````````
-:n:`{? Local | Global | Export }`
+:n:`{? {| Local | Global | Export } }`
Flag and option settings can be global in scope or local to nested scopes created by
:cmd:`Module` and :cmd:`Section` commands. There are four alternatives:
@@ -277,7 +277,7 @@ Requests to the environment
:token:`term_pattern` (holes of the pattern are either denoted by `_` or by
:n:`?@ident` when non linear patterns are expected).
- .. cmdv:: Search { + [-]@term_pattern_string }
+ .. cmdv:: Search {+ {? -}@term_pattern_string}
where
:n:`@term_pattern_string` is a term_pattern, a string, or a string followed
@@ -289,17 +289,17 @@ Requests to the environment
prefixed by `-`, the search excludes the objects that mention that
term_pattern or that string.
- .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid }
+ .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid }
This restricts the search to constructions defined in the modules
named by the given :n:`qualid` sequence.
- .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }
+ .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid }
This restricts the search to constructions not defined in the modules
named by the given :n:`qualid` sequence.
- .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string
+ .. cmdv:: @selector: Search {+ {? -}@term_pattern_string}
This specifies the goal on which to search hypothesis (see
Section :ref:`invocation-of-tactics`).
@@ -353,7 +353,7 @@ Requests to the environment
This restricts the search to constructions defined in the modules named
by the given :n:`qualid` sequence.
- .. cmdv:: SearchHead term outside {+ @qualid }
+ .. cmdv:: SearchHead @term outside {+ @qualid }
This restricts the search to constructions not defined in the modules
named by the given :n:`qualid` sequence.
@@ -443,7 +443,7 @@ Requests to the environment
SearchRewrite (_ + _ + _).
- .. cmdv:: SearchRewrite term inside {+ @qualid }
+ .. cmdv:: SearchRewrite @term inside {+ @qualid }
This restricts the search to constructions defined in the modules
named by the given :n:`qualid` sequence.
@@ -622,7 +622,7 @@ file is a particular case of module called *library file*.
but if a further module, say `A`, contains a command :cmd:`Require Export` `B`,
then the command :cmd:`Require Import` `A` also imports the module `B.`
- .. cmdv:: Require [Import | Export] {+ @qualid }
+ .. cmdv:: Require {| Import | Export } {+ @qualid }
This loads the
modules named by the :token:`qualid` sequence and their recursive
@@ -988,7 +988,7 @@ Controlling display
This option controls the normal displaying.
-.. opt:: Warnings "{+, {? %( - %| + %) } @ident }"
+.. opt:: Warnings "{+, {? {| - | + } } @ident }"
:name: Warnings
This option configures the display of warnings. It is experimental, and
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 418922e9b3..3a12ee288a 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme``
Generation of inversion principles with ``Derive`` ``Inversion``
-----------------------------------------------------------------
-.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort
+.. cmd:: Derive Inversion @ident with @ident Sort @sort
+ Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort
This command generates an inversion principle for the
- :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive
- predicate and :g:`x` the variables occurring in t. This command
- generates and stocks the inversion lemma for the sort :g:`sort`
- corresponding to the instance :g:`∀ (x:T), I t` with the name
- :n:`@ident` in the global environment. When applied, it is
- equivalent to having inverted the instance with the tactic
- :g:`inversion`.
-
+ :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name
+ of the generated principle. The second :token:`ident` should be an inductive
+ predicate, and :token:`binders` the variables occurring in the term
+ :token:`term`. This command generates the inversion lemma for the sort
+ :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`.
+ When applied, it is equivalent to having inverted the instance with the
+ tactic :g:`inversion`.
-.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
+ Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
When applied, it is equivalent to having inverted the instance with the
tactic inversion replaced by the tactic `inversion_clear`.
-.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort
+ Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort
When applied, it is equivalent to having inverted the instance with
the tactic `dependent inversion`.
-.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort
+ Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
When applied, it is equivalent to having inverted the instance
with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index edec13f681..cda228a7da 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -327,22 +327,29 @@ symbols.
Reserving notations
~~~~~~~~~~~~~~~~~~~
-A given notation may be used in different contexts. Coq expects all
-uses of the notation to be defined at the same precedence and with the
-same associativity. To avoid giving the precedence and associativity
-every time, it is possible to declare a parsing rule in advance
-without giving its interpretation. Here is an example from the initial
-state of Coq.
+.. cmd:: Reserved Notation @string {? (@modifiers) }
-.. coqtop:: in
+ A given notation may be used in different contexts. Coq expects all
+ uses of the notation to be defined at the same precedence and with the
+ same associativity. To avoid giving the precedence and associativity
+ every time, this command declares a parsing rule (:token:`string`) in advance
+ without giving its interpretation. Here is an example from the initial
+ state of Coq.
+
+ .. coqtop:: in
+
+ Reserved Notation "x = y" (at level 70, no associativity).
+
+ Reserving a notation is also useful for simultaneously defining an
+ inductive type or a recursive constant and a notation for it.
- Reserved Notation "x = y" (at level 70, no associativity).
+ .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
+ their precedence and associativity cannot be changed.
-Reserving a notation is also useful for simultaneously defining an
-inductive type or a recursive constant and a notation for it.
+ .. cmdv:: Reserved Infix "@symbol" {* @modifiers}
-.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
- their precedence and associativity cannot be changed.
+ This command declares an infix parsing rule without giving its
+ interpretation.
Simultaneous definition of terms and notations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 22:54:40 +0000