diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 90 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 494 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 204 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 28 |
6 files changed, 437 insertions, 420 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index f18569c7fd..8663ac646b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|. We start by giving the syntax followed by the informal semantics. To learn more about the language and especially about its foundations, please refer to :cite:`Del00`. -(Note the examples in the paper won't work as-is; Coq has evolved +(Note the examples in the paper won't work as-is; |Coq| has evolved since the paper was written.) .. example:: Basic tactic macros @@ -41,7 +41,7 @@ higher precedence than `+`. Usually `a/b/c` is given the :gdef:`left associativ interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation `a/(b/c)`. -In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` +In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4` because `||` is part of :token:`ltac_expr2`, which has higher precedence than :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which @@ -161,7 +161,7 @@ Syntactic values Provides a way to use the syntax and semantics of a grammar nonterminal as a value in an :token:`ltac_expr`. The table below describes the most useful of these. You can see the others by running ":cmd:`Print Grammar` `tactic`" and -examining the part at the end under "Entry tactic:tactic_arg". +examining the part at the end under "Entry tactic:tactic_value". :token:`ident` name of a grammar nonterminal listed in the table @@ -784,7 +784,7 @@ single success: Checking for a single success: exactly_once ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Coq provides an experimental way to check that a tactic has *exactly +|Coq| provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @ltac_expr3 @@ -813,7 +813,7 @@ one* success: Checking for failure: assert_fails ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: +|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr3 :name: assert_fails @@ -859,7 +859,7 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: Checking for success: assert_succeeds ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* +|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @ltac_expr3 @@ -879,7 +879,8 @@ Print/identity tactic: idtac .. tacn:: idtac {* {| @ident | @string | @natural } } :name: idtac - Leaves the proof unchanged and prints the given tokens. Strings and integers are printed + Leaves the proof unchanged and prints the given tokens. :token:`String<string>`\s + and :token:`natural`\s are printed literally. If :token:`ident` is an |Ltac| variable, its contents are printed; if not, it is an error. @@ -888,7 +889,7 @@ Print/identity tactic: idtac Failing ~~~~~~~ -.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @integer } } +.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @natural } } :name: fail; gfail :tacn:`fail` is the always-failing tactic: it does not solve any @@ -904,7 +905,7 @@ Failing See the example for a comparison of the two constructs. - Note that if Coq terms have to be + Note that if |Coq| terms have to be printed as part of the failure, term construction always forces the tactic into the goals, meaning that if there are no goals when it is evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed. @@ -919,7 +920,7 @@ Failing the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct, respecting the algebraic identity. - :n:`{* {| @ident | @string | @integer } }` + :n:`{* {| @ident | @string | @natural } }` The given tokens are used for printing the failure message. If :token:`ident` is an |Ltac| variable, its contents are printed; if not, it is an error. @@ -937,7 +938,7 @@ Failing .. todo the example is too long; could show the Goal True. Proof. once and hide the Aborts to shorten it. And add a line of text before each subexample. Perhaps add some very short - explanations/generalizations (eg gfail always fails; "tac; fail" succeeds but "fail." alone + explanations/generalizations (e.g. gfail always fails; "tac; fail" succeeds but "fail." alone fails. .. coqtop:: reset all fail @@ -989,7 +990,7 @@ amount of time: timeout with some other tacticals. This tactical is hence proposed only for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that - this tactical isn’t available on the native Windows port of Coq. + this tactical isn’t available on the native Windows port of |Coq|. Timing a tactic ~~~~~~~~~~~~~~~ @@ -1488,7 +1489,7 @@ Examples: match_context_rule ::= [ {*, @match_hyp } |- @match_pattern ] => @ltac_expr match_hyp ::= | @name := {? [ @match_pattern ] : } @match_pattern -.. todo PR The following items (up to numgoals) are part of "value_tactic". I'd like to make +.. todo The following items (up to numgoals) are part of "value_tactic". I'd like to make this a subsection and explain that they all return values. How do I get a 5th-level section title? Filling a term context @@ -1884,7 +1885,7 @@ Proving that a list is a permutation of a second list From Section :ref:`ltac-syntax` we know that Ltac has a primitive notion of integers, but they are only used as arguments for primitive tactics and we cannot make computations with them. Thus, - instead, we use Coq's natural number type :g:`nat`. + instead, we use |Coq|'s natural number type :g:`nat`. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 773e393eb6..41f376c43d 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -3,8 +3,8 @@ Ltac2 ===== -The Ltac tactic language is probably one of the ingredients of the success of -Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: +The |Ltac| tactic language is probably one of the ingredients of the success of +|Coq|, yet it is at the same time its Achilles' heel. Indeed, |Ltac|: - has often unclear semantics - is very non-uniform due to organic growth @@ -30,7 +30,7 @@ as Ltac1. Current limitations include: - There are a number of tactics that are not yet supported in Ltac2 because - the interface OCaml and/or Ltac2 notations haven't been written. See + the interface |OCaml| and/or Ltac2 notations haven't been written. See :ref:`defining_tactics`. - Missing usability features such as: @@ -38,7 +38,6 @@ Current limitations include: - Printing functions are limited and awkward to use. Only a few data types are printable. - Deep pattern matching and matching on tuples don't work. - - If statements on Ltac2 boolean values - A convenient way to build terms with casts through the low-level API. Because the cast type is opaque, building terms with casts currently requires an awkward construction like the following, which also incurs extra overhead to repeat typechecking for each @@ -90,7 +89,7 @@ In particular, Ltac2 is: * together with the Hindley-Milner type system - a language featuring meta-programming facilities for the manipulation of - Coq-side terms + |Coq|-side terms - a language featuring notation facilities to help write palatable scripts We describe these in more detail in the remainder of this document. @@ -108,14 +107,14 @@ that ML constitutes a sweet spot in PL design, as it is relatively expressive while not being either too lax (unlike dynamic typing) nor too strict (unlike, say, dependent types). -The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it +The main goal of Ltac2 is to serve as a meta-language for |Coq|. As such, it naturally fits in the ML lineage, just as the historical ML was designed as the tactic language for the LCF prover. It can also be seen as a general-purpose -language, by simply forgetting about the Coq-specific features. +language, by simply forgetting about the |Coq|-specific features. Sticking to a standard ML type system can be considered somewhat weak for a -meta-language designed to manipulate Coq terms. In particular, there is no -way to statically guarantee that a Coq term resulting from an Ltac2 +meta-language designed to manipulate |Coq| terms. In particular, there is no +way to statically guarantee that a |Coq| term resulting from an Ltac2 computation will be well-typed. This is actually a design choice, motivated by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are @@ -138,7 +137,7 @@ Type Syntax ~~~~~~~~~~~ At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to OCaml. Types follow the simply-typed syntax of OCaml. +close to |OCaml|. Types follow the simply-typed syntax of |OCaml|. .. insertprodn ltac2_type ltac2_typevar @@ -160,7 +159,7 @@ declarations such as algebraic datatypes and records. Built-in types include: -- ``int``, machine integers (size not specified, in practice inherited from OCaml) +- ``int``, machine integers (size not specified, in practice inherited from |OCaml|) - ``string``, mutable strings - ``'a array``, mutable arrays - ``exn``, exceptions @@ -201,7 +200,7 @@ One can define new types with the following commands. :token:`tac2typ_knd` should be in the form :n:`[ {? {? %| } {+| @tac2alg_constructor } } ]`. Without :n:`{| := | ::= }` - Defines an abstract type for use representing data from OCaml. Not for + Defines an abstract type for use representing data from |OCaml|. Not for end users. :n:`with @tac2typ_def` @@ -227,9 +226,9 @@ One can define new types with the following commands. .. cmd:: Ltac2 @ external @ident : @ltac2_type := @string @string :name: Ltac2 external - Declares abstract terms. Frequently, these declare OCaml functions + Declares abstract terms. Frequently, these declare |OCaml| functions defined in |Coq| and give their type information. They can also declare - data structures from OCaml. This command has no use for the end user. + data structures from |OCaml|. This command has no use for the end user. APIs ~~~~ @@ -345,12 +344,10 @@ Ltac2 Definitions .. coqtop:: all - Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. - Ltac2 Set f := fun b => - match b with true => 1 | _ => f true end. + Ltac2 mutable rec f b := if b then 0 else f true. + Ltac2 Set f := fun b => if b then 1 else f true. Ltac2 Eval (f false). - Ltac2 Set f as oldf := fun b => - match b with true => 2 | _ => oldf false end. + Ltac2 Set f as oldf := fun b => if b then 2 else oldf false. Ltac2 Eval (f false). In the definition, the `f` in the body is resolved statically @@ -363,7 +360,7 @@ Reduction ~~~~~~~~~ We use the usual ML call-by-value reduction, with an otherwise unspecified -evaluation order. This is a design choice making it compatible with OCaml, +evaluation order. This is a design choice making it compatible with |OCaml|, if ever we implement native compilation. The expected equations are as follows:: (fun x => t) V ≡ t{x := V} (βv) @@ -407,7 +404,7 @@ standard IO monad as the ambient effectful world, Ltac2 is has a tactic monad. Note that the order of evaluation of application is *not* specified and is -implementation-dependent, as in OCaml. +implementation-dependent, as in |OCaml|. We recall that the `Proofview.tactic` monad is essentially a IO monad together with backtracking state representing the proof state. @@ -537,8 +534,8 @@ aware of bound variables and must use heuristics to decide whether a variable is a proper one or referring to something in the Ltac context. Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is -not ``foo`` applied to the Ltac integer expression ``0`` (Ltac does have a -notion of integers, though it is not first-class), but rather the Coq term +not ``foo`` applied to the Ltac integer expression ``0`` (|Ltac| does have a +notion of integers, though it is not first-class), but rather the |Coq| term :g:`Datatypes.O`. The implicit parsing is confusing to users and often gives unexpected results. @@ -570,11 +567,11 @@ Built-in quotations The current implementation recognizes the following built-in quotations: - ``ident``, which parses identifiers (type ``Init.ident``). -- ``constr``, which parses Coq terms and produces an-evar free term at runtime +- ``constr``, which parses |Coq| terms and produces an-evar free term at runtime (type ``Init.constr``). -- ``open_constr``, which parses Coq terms and produces a term potentially with +- ``open_constr``, which parses |Coq| terms and produces a term potentially with holes at runtime (type ``Init.constr`` as well). -- ``pattern``, which parses Coq patterns and produces a pattern used for term +- ``pattern``, which parses |Coq| patterns and produces a pattern used for term matching (type ``Init.pattern``). - ``reference`` Qualified names are globalized at internalization into the corresponding global reference, @@ -617,7 +614,7 @@ Term Antiquotations Syntax ++++++ -One can also insert Ltac2 code into Coq terms, similar to what is possible in +One can also insert Ltac2 code into |Coq| terms, similar to what is possible in Ltac1. .. prodn:: @@ -629,7 +626,7 @@ for their side-effects. Semantics +++++++++ -A quoted Coq term is interpreted in two phases, internalization and +A quoted |Coq| term is interpreted in two phases, internalization and evaluation. - Internalization is part of the static semantics, that is, it is done at Ltac2 @@ -637,17 +634,17 @@ evaluation. - Evaluation is part of the dynamic semantics, that is, it is done when a term gets effectively computed by Ltac2. -Note that typing of Coq terms is a *dynamic* process occurring at Ltac2 +Note that typing of |Coq| terms is a *dynamic* process occurring at Ltac2 evaluation time, and not at Ltac2 typing time. Static semantics **************** -During internalization, Coq variables are resolved and antiquotations are -type checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq +During internalization, |Coq| variables are resolved and antiquotations are +type checked as Ltac2 terms, effectively producing a ``glob_constr`` in |Coq| implementation terminology. Note that although it went through the type checking of **Ltac2**, the resulting term has not been fully computed and -is potentially ill-typed as a runtime **Coq** term. +is potentially ill-typed as a runtime **|Coq|** term. .. example:: @@ -669,7 +666,7 @@ of the corresponding term expression. let x := '0 in constr:(1 + ltac2:(exact x)) Beware that the typing environment of antiquotations is **not** -expanded by the Coq binders from the term. +expanded by the |Coq| binders from the term. .. example:: @@ -692,17 +689,17 @@ as follows. `constr:(fun x : nat => ltac2:(exact (hyp @x)))` -This pattern is so common that we provide dedicated Ltac2 and Coq term notations +This pattern is so common that we provide dedicated Ltac2 and |Coq| term notations for it. - `&x` as an Ltac2 expression expands to `hyp @x`. -- `&x` as a Coq constr expression expands to +- `&x` as a |Coq| constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. -In the special case where Ltac2 antiquotations appear inside a Coq term +In the special case where Ltac2 antiquotations appear inside a |Coq| term notation, the notation variables are systematically bound in the body of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents -untyped syntactic Coq expressions, which can by typed in the +untyped syntactic |Coq| expressions, which can by typed in the current context using the `Ltac2.Constr.pretype` function. .. example:: @@ -748,9 +745,9 @@ the notation section. .. prodn:: term += $@lident -In a Coq term, writing :g:`$x` is semantically equivalent to +In a |Coq| term, writing :g:`$x` is semantically equivalent to :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to -insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term. +insert in a concise way an Ltac2 variable of type :n:`constr` into a |Coq| term. Match over terms ~~~~~~~~~~~~~~~~ @@ -1129,7 +1126,7 @@ Match on values .. tacn:: match @ltac2_expr5 with {? @ltac2_branches } end :name: match (Ltac2) - Matches a value, akin to the OCaml `match` construct. By itself, it doesn't cause backtracking + Matches a value, akin to the |OCaml| `match` construct. By itself, it doesn't cause backtracking as do the `*match*!` and `*match*! goal` constructs. .. insertprodn ltac2_branches atomic_tac2pat @@ -1149,6 +1146,13 @@ Match on values | @tac2pat1 , {*, @tac2pat1 } | @tac2pat1 +.. tacn:: if @ltac2_expr5__test then @ltac2_expr5__then else @ltac2_expr5__else + :name: if-then-else (Ltac2) + + Equivalent to a :tacn:`match <match (Ltac2)>` on a boolean value. If the + :n:`@ltac2_expr5__test` evaluates to true, :n:`@ltac2_expr5__then` + is evaluated. Otherwise :n:`@ltac2_expr5__else` is evaluated. + .. note:: For now, deep pattern matching is not implemented. @@ -1254,7 +1258,7 @@ Abbreviations Introduces a special kind of notation, called an abbreviation, that does not add any parsing rules. It is similar in - spirit to Coq abbreviations (see :cmd:`Notation (abbreviation)`, + spirit to |Coq| abbreviations (see :cmd:`Notation (abbreviation)`, insofar as its main purpose is to give an absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition. @@ -1281,7 +1285,7 @@ Abbreviations Defining tactics ~~~~~~~~~~~~~~~~ -Built-in tactics (those defined in OCaml code in the |Coq| executable) and Ltac1 tactics, +Built-in tactics (those defined in |OCaml| code in the |Coq| executable) and Ltac1 tactics, which are defined in `.v` files, must be defined through notations. (Ltac2 tactics can be defined with :cmd:`Ltac2`. @@ -1795,7 +1799,7 @@ Transition from Ltac1 Owing to the use of a lot of notations, the transition should not be too difficult. In particular, it should be possible to do it incrementally. That said, we do *not* guarantee it will be a blissful walk either. -Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq +Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with |Coq| will help you. We list the major changes and the transition strategies hereafter. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f722ddda79..f4aef8f879 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -11,7 +11,7 @@ section. They can also use some other specialized commands called *tactics*. They are the very tools allowing the user to deal with logical reasoning. They are documented in Chapter :ref:`tactics`. -Coq user interfaces usually have a way of marking whether the user has +|Coq| user interfaces usually have a way of marking whether the user has switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into :n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. @@ -36,7 +36,7 @@ terms are called *proof terms*. .. exn:: No focused proof. - Coq raises this error message when one attempts to use a proof editing command + |Coq| raises this error message when one attempts to use a proof editing command out of the proof editing mode. .. _proof-editing-mode: @@ -49,7 +49,7 @@ the assertion of a theorem using an assertion command like :cmd:`Theorem`. The list of assertion commands is given in :ref:`Assertions`. The command :cmd:`Goal` can also be used. -.. cmd:: Goal @form +.. cmd:: Goal @type This is intended for quick assertion of statements, without knowing in advance which name to give to the assertion, typically for quick @@ -62,8 +62,8 @@ list of assertion commands is given in :ref:`Assertions`. The command This command is available in interactive editing proof mode when the proof is completed. Then :cmd:`Qed` extracts a proof term from the proof - script, switches back to Coq top-level and attaches the extracted - proof term to the declared name of the original goal. This name is + script, switches back to |Coq| top-level and attaches the extracted + proof term to the declared name of the original goal. The name is added to the environment as an opaque constant. .. exn:: Attempt to save an incomplete proof. @@ -80,42 +80,42 @@ list of assertion commands is given in :ref:`Assertions`. The command a while when the proof is large. In some exceptional cases one may even incur a memory overflow. -.. cmd:: Defined - - Same as :cmd:`Qed`, except the proof is made *transparent*, which means - that its content can be explicitly used for type checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). - .. cmd:: Save @ident :name: Save - Saves a completed proof with the name :token:`ident`. + Saves a completed proof with the name :token:`ident`, which + overrides any name provided by the :cmd:`Theorem` command or + its variants. + +.. cmd:: Defined {? @ident } + + Similar to :cmd:`Qed` and :cmd:`Save`, except the proof is made *transparent*, which means + that its content can be explicitly used for type checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). If :token:`ident` is specified, + the proof is defined with the given name, which overrides any name + provided by the :cmd:`Theorem` command or its variants. .. cmd:: Admitted This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom. -.. cmd:: Abort +.. cmd:: Abort {? {| All | @ident } } - This command cancels the current proof development, switching back to + Cancels the current proof development, switching back to the previous proof development, or to the |Coq| toplevel if no other - proof was edited. - - .. exn:: No focused proof (No proof-editing in progress). - :undocumented: - - .. cmdv:: Abort @ident - - Aborts the editing of the proof named :token:`ident` (in case you have - nested proofs). + proof was being edited. - .. seealso:: :flag:`Nested Proofs Allowed` + :n:`@ident` + Aborts editing the proof named :n:`@ident` for use when you have + nested proofs. See also :flag:`Nested Proofs Allowed`. - .. cmdv:: Abort All + :n:`All` + Aborts all current proofs. - Aborts all current goals. + .. exn:: No focused proof (No proof-editing in progress). + :undocumented: .. cmd:: Proof @term :name: Proof `term` @@ -143,12 +143,26 @@ list of assertion commands is given in :ref:`Assertions`. The command .. seealso:: :cmd:`Proof with` -.. cmd:: Proof using {+ @ident } +.. cmd:: Proof using @section_var_expr {? with @ltac_expr } + + .. insertprodn section_var_expr starred_ident_ref - This command applies in proof editing mode. It declares the set of + .. prodn:: + section_var_expr ::= {* @starred_ident_ref } + | {? - } @section_var_expr50 + section_var_expr50 ::= @section_var_expr0 - @section_var_expr0 + | @section_var_expr0 + @section_var_expr0 + | @section_var_expr0 + section_var_expr0 ::= @starred_ident_ref + | ( @section_var_expr ) {? * } + starred_ident_ref ::= @ident {? * } + | Type {? * } + | All + + Opens proof editing mode, declaring the set of section variables (see :ref:`gallina-assumptions`) used by the proof. At :cmd:`Qed` time, the - system will assert that the set of section variables actually used in + system verifies that the set of section variables used in the proof is a subset of the declared one. The set of declared variables is closed under type dependency. For @@ -160,50 +174,55 @@ list of assertion commands is given in :ref:`Assertions`. The command the statement. In other words ``Proof using e`` is equivalent to ``Proof using Type + e`` for any declaration expression ``e``. - .. cmdv:: Proof using {+ @ident } with @tactic - - Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`. - - .. seealso:: :ref:`tactics-implicit-automation` + :n:`- @section_var_expr50` + Use all section variables except those specified by :n:`@section_var_expr50` - .. cmdv:: Proof using All + :n:`@section_var_expr0 + @section_var_expr0` + Use section variables from the union of both collections. + See :ref:`nameaset` to see how to form a named collection. - Use all section variables. + :n:`@section_var_expr0 - @section_var_expr0` + Use section variables which are in the first collection but not in the + second one. - .. cmdv:: Proof using {? Type } + :n:`{? * }` + Use the transitive closure of the specified collection. - Use only section variables occurring in the statement. + :n:`Type` + Use only section variables occurring in the statement. Specifying :n:`*` + uses the forward transitive closure of all the section variables occurring + in the statement. For example, if the variable ``H`` has type ``p < 5`` then + ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``. - .. cmdv:: Proof using Type* + :n:`All` + Use all section variables. - The ``*`` operator computes the forward transitive closure. E.g. if the - variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type - of ``H``. ``Type*`` is the forward transitive closure of the entire set of - section variables occurring in the statement. + .. seealso:: :ref:`tactics-implicit-automation` - .. cmdv:: Proof using -({+ @ident }) +.. attr:: using - Use all section variables except the list of :token:`ident`. + This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`, + :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and + its variants. It takes + a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to + specifying the same :n:`@section_var_expr` in + :cmd:`Proof using`. - .. cmdv:: Proof using @collection__1 + @collection__2 - - Use section variables from the union of both collections. - See :ref:`nameaset` to know how to form a named collection. - - .. cmdv:: Proof using @collection__1 - @collection__2 + .. example:: - Use section variables which are in the first collection but not in the - second one. + .. coqtop:: all - .. cmdv:: Proof using @collection - ({+ @ident }) + Section Test. + Variable n : nat. + Hypothesis Hn : n <> 0. - Use section variables which are in the first collection but not in the - list of :token:`ident`. + #[using="Hn"] + Lemma example : 0 < n. - .. cmdv:: Proof using @collection * + .. coqtop:: in - Use section variables in the forward transitive closure of the collection. - The ``*`` operator binds stronger than ``+`` and ``-``. + Abort. + End Test. Proof using options @@ -212,10 +231,10 @@ Proof using options The following options modify the behavior of ``Proof using``. -.. opt:: Default Proof Using "@collection" +.. opt:: Default Proof Using "@section_var_expr" :name: Default Proof Using - Use :n:`@collection` as the default ``Proof using`` value. E.g. ``Set Default + Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. @@ -230,7 +249,7 @@ The following options modify the behavior of ``Proof using``. Name a set of section hypotheses for ``Proof using`` ```````````````````````````````````````````````````` -.. cmd:: Collection @ident := @collection +.. cmd:: Collection @ident := @section_var_expr This can be used to name a set of section hypotheses, with the purpose of making ``Proof using`` annotations more @@ -259,7 +278,7 @@ Name a set of section hypotheses for ``Proof using`` -.. cmd:: Existential @natural := @term +.. cmd:: Existential @natural {? : @type } := @term This command instantiates an existential variable. :token:`natural` is an index in the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. @@ -285,64 +304,60 @@ their own proof modes. The default proof mode used when opening a proof can be changed using the following option. .. opt:: Default Proof Mode @string - :name: Default Proof Mode Select the proof mode to use when starting a proof. Depending on the proof mode, various syntactic constructs are allowed when writing an interactive - proof. The possible option values are listed below. - - - "Classic": this is the default. It activates the |Ltac| language to interact - with the proof, and also allows vernacular commands. - - - "Noedit": this proof mode only allows vernacular commands. No tactic - language is activated at all. This is the default when the prelude is not - loaded, e.g. through the `-noinit` option for `coqc`. - - - "Ltac2": this proof mode is made available when requiring the Ltac2 - library, and is set to be the default when it is imported. It allows - to use the Ltac2 language, as well as vernacular commands. - - - Some external plugins also define their own proof mode, which can be - activated via this command. + proof. All proof modes support vernacular commands; the proof mode determines + which tactic language and set of tactic definitions are available. The + possible option values are: + + `"Classic"` + Activates the |Ltac| language and the tactics with the syntax documented + in this manual. + Some tactics are not available until the associated plugin is loaded, + such as `SSR` or `micromega`. + This proof mode is set when the :term:`prelude` is loaded. + + `"Noedit"` + No tactic + language is activated at all. This is the default when the :term:`prelude` + is not loaded, e.g. through the `-noinit` option for `coqc`. + + `"Ltac2"` + Activates the Ltac2 language and the Ltac2-specific variants of the documented + tactics. + This value is only available after :cmd:`Requiring <Require>` Ltac2. + :cmd:`Importing <Import>` Ltac2 sets this mode. + + Some external plugins also define their own proof mode, which can be + activated with this command. Navigation in the proof tree -------------------------------- -.. cmd:: Undo - - This command cancels the effect of the last command. Thus, it - backtracks one step. - -.. cmdv:: Undo @natural +.. cmd:: Undo {? {? To } @natural } - Repeats Undo :token:`natural` times. + Cancels the effect of the last :token:`natural` commands or tactics. + The :n:`To @natural` form goes back to the specified state number. + If :token:`natural` is not specified, the command goes back one command or tactic. -.. cmdv:: Restart - :name: Restart +.. cmd:: Restart - This command restores the proof editing process to the original goal. + Restores the proof editing process to the original goal. .. exn:: No focused proof to restart. :undocumented: -.. cmd:: Focus +.. cmd:: Focus {? @natural } - This focuses the attention on the first subgoal to prove and the + Focuses the attention on the first subgoal to prove or, if :token:`natural` is + specified, the :token:`natural`\-th. The printing of the other subgoals is suspended until the focused subgoal - is solved or unfocused. This is useful when there are many current - subgoals which clutter your screen. - - .. deprecated:: 8.8 - - Prefer the use of bullets or focusing brackets (see below). - -.. cmdv:: Focus @natural - - This focuses the attention on the :token:`natural` th subgoal to prove. + is solved or unfocused. .. deprecated:: 8.8 - Prefer the use of focusing brackets with a goal selector (see below). + Prefer the use of bullets or focusing brackets with a goal selector (see below). .. cmd:: Unfocus @@ -361,11 +376,19 @@ Navigation in the proof tree .. index:: { } -.. cmd:: {| %{ | %} } +.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket, + hence the verbose names + +.. tacn:: {? {| @natural | [ @ident ] } : } %{ + %} - The command ``{`` (without a terminating period) focuses on the first - goal, much like :cmd:`Focus` does, however, the subproof can only be - unfocused when it has been fully solved ( *i.e.* when there is no + .. todo + See https://github.com/coq/coq/issues/12004 and + https://github.com/coq/coq/issues/12825. + + ``{`` (without a terminating period) focuses on the first + goal. The subproof can only be + unfocused when it has been fully solved (*i.e.*, when there is no focused goal left). Unfocusing is then handled by ``}`` (again, without a terminating period). See also an example in the next section. @@ -373,67 +396,65 @@ Navigation in the proof tree together with a suggestion about the right bullet or ``}`` to unfocus it or focus the next one. - .. cmdv:: @natural: %{ - - This focuses on the :token:`natural`\-th subgoal to prove. - - .. cmdv:: [@ident]: %{ + :n:`@natural:` + Focuses on the :token:`natural`\-th subgoal to prove. - This focuses on the named goal :token:`ident`. + :n:`[ @ident ]: %{` + Focuses on the named goal :token:`ident`. - .. note:: + .. note:: - Goals are just existential variables and existential variables do not - get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. - You may also wrap this in an Ltac-definition like: + Goals are just existential variables and existential variables do not + get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + You may also wrap this in an Ltac-definition like: - .. coqtop:: in + .. coqtop:: in - Ltac name_goal name := refine ?[name]. + Ltac name_goal name := refine ?[name]. - .. seealso:: :ref:`existential-variables` + .. seealso:: :ref:`existential-variables` - .. example:: + .. example:: - This first example uses the Ltac definition above, and the named goals - only serve for documentation. + This first example uses the Ltac definition above, and the named goals + only serve for documentation. - .. coqtop:: all + .. coqtop:: all - Goal forall n, n + 0 = n. - Proof. - induction n; [ name_goal base | name_goal step ]. - [base]: { + Goal forall n, n + 0 = n. + Proof. + induction n; [ name_goal base | name_goal step ]. + [base]: { - .. coqtop:: all + .. coqtop:: all - reflexivity. + reflexivity. - .. coqtop:: in + .. coqtop:: in - } + } - .. coqtop:: all + .. coqtop:: all - [step]: { + [step]: { - .. coqtop:: all + .. coqtop:: all - simpl. - f_equal. - assumption. - } - Qed. + simpl. + f_equal. + assumption. + } + Qed. - This can also be a way of focusing on a shelved goal, for instance: + This can also be a way of focusing on a shelved goal, for instance: - .. coqtop:: all + .. coqtop:: all - Goal exists n : nat, n = n. - eexists ?[x]. - reflexivity. - [x]: exact 0. - Qed. + Goal exists n : nat, n = n. + eexists ?[x]. + reflexivity. + [x]: exact 0. + Qed. .. exn:: This proof is focused, but cannot be unfocused this way. @@ -450,14 +471,14 @@ Navigation in the proof tree Brackets are used to focus on a single goal given either by its position or by its name if it has one. - .. seealso:: The error messages about bullets below. + .. seealso:: The error messages for bullets below. .. _bullets: Bullets ``````` -Alternatively to ``{`` and ``}``, proofs can be structured with bullets. The +Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The use of a bullet ``b`` for the first time focuses on the first goal ``g``, the same bullet cannot be used again until the proof of ``g`` is completed, then it is mandatory to focus the next goal with ``b``. The consequence is @@ -552,111 +573,103 @@ Requesting information ---------------------- -.. cmd:: Show - - This command displays the current goals. - - .. exn:: No focused proof. - :undocumented: +.. cmd:: Show {? {| @ident | @natural } } - .. cmdv:: Show @natural + Displays the current goals. - Displays only the :token:`natural`\-th subgoal. + :n:`@natural` + Display only the :token:`natural`\-th subgoal. - .. exn:: No such goal. - :undocumented: + :n:`@ident` + Displays the named goal :token:`ident`. This is useful in + particular to display a shelved goal but only works if the + corresponding existential variable has been named by the user + (see :ref:`existential-variables`) as in the following example. - .. cmdv:: Show @ident + .. example:: - Displays the named goal :token:`ident`. This is useful in - particular to display a shelved goal but only works if the - corresponding existential variable has been named by the user - (see :ref:`existential-variables`) as in the following example. + .. coqtop:: all abort - .. example:: + Goal exists n, n = 0. + eexists ?[n]. + Show n. - .. coqtop:: all abort + .. exn:: No focused proof. + :undocumented: - Goal exists n, n = 0. - eexists ?[n]. - Show n. + .. exn:: No such goal. + :undocumented: - .. cmdv:: Show Proof {? Diffs {? removed } } - :name: Show Proof +.. cmd:: Show Proof {? Diffs {? removed } } - Displays the proof term generated by the tactics - that have been applied so far. If the proof is incomplete, the term - will contain holes, which correspond to subterms which are still to be - constructed. Each hole is an existential variable, which appears as a - question mark followed by an identifier. + Displays the proof term generated by the tactics + that have been applied so far. If the proof is incomplete, the term + will contain holes, which correspond to subterms which are still to be + constructed. Each hole is an existential variable, which appears as a + question mark followed by an identifier. - Specifying “Diffs” highlights the difference between the - current and previous proof step. By default, the command shows the - output once with additions highlighted. Including “removed” shows - the output twice: once showing removals and once showing additions. - It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. + Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. - .. cmdv:: Show Conjectures - :name: Show Conjectures +.. cmd:: Show Conjectures - It prints the list of the names of all the - theorems that are currently being proved. As it is possible to start - proving a previous lemma during the proof of a theorem, this list may - contain several names. + Prints the names of all the + theorems that are currently being proved. As it is possible to start + proving a previous lemma during the proof of a theorem, there may + be multiple names. - .. cmdv:: Show Intro - :name: Show Intro +.. cmd:: Show Intro - If the current goal begins by at least one product, - this command prints the name of the first product, as it would be - generated by an anonymous :tacn:`intro`. The aim of this command is to ease - the writing of more robust scripts. For example, with an appropriate - Proof General macro, it is possible to transform any anonymous :tacn:`intro` - into a qualified one such as ``intro y13``. In the case of a non-product - goal, it prints nothing. + If the current goal begins by at least one product, + prints the name of the first product as it would be + generated by an anonymous :tacn:`intro`. The aim of this command is to ease + the writing of more robust scripts. For example, with an appropriate + Proof General macro, it is possible to transform any anonymous :tacn:`intro` + into a qualified one such as ``intro y13``. In the case of a non-product + goal, it prints nothing. - .. cmdv:: Show Intros - :name: Show Intros +.. cmd:: Show Intros - This command is similar to the previous one, it - simulates the naming process of an :tacn:`intros`. + Similar to the previous command. + Simulates the naming process of :tacn:`intros`. - .. cmdv:: Show Existentials - :name: Show Existentials +.. cmd:: Show Existentials - Displays all open goals / existential variables in the current proof - along with the type and the context of each variable. + Displays all open goals / existential variables in the current proof + along with the type and the context of each variable. - .. cmdv:: Show Match @ident +.. cmd:: Show Match @qualid - This variant displays a template of the Gallina - ``match`` construct with a branch for each constructor of the type - :token:`ident` + Displays a template of the Gallina :token:`match<term_match>` + construct with a branch for each constructor of the type + :token:`qualid`. This is used internally by + `company-coq <https://github.com/cpitclaudel/company-coq>`_. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Show Match nat. + Show Match nat. - .. exn:: Unknown inductive type. - :undocumented: + .. exn:: Unknown inductive type. + :undocumented: - .. cmdv:: Show Universes - :name: Show Universes +.. cmd:: Show Universes - It displays the set of all universe constraints and - its normalized form at the current stage of the proof, useful for - debugging universe inconsistencies. + Displays the set of all universe constraints and + its normalized form at the current stage of the proof, useful for + debugging universe inconsistencies. - .. cmdv:: Show Goal @natural at @natural - :name: Show Goal +.. cmd:: Show Goal @natural at @natural - This command is only available in coqtop. Displays a goal at a - proof state using the goal ID number and the proof state ID number. - It is primarily for use by tools such as Prooftree that need to fetch - goal history in this way. Prooftree is a tool for visualizing a proof - as a tree that runs in Proof General. + Available in coqtop. Displays a goal at a + proof state using the goal ID number and the proof state ID number. + It is primarily for use by tools such as Prooftree that need to fetch + goal history in this way. Prooftree is a tool for visualizing a proof + as a tree that runs in Proof General. .. cmd:: Guarded @@ -675,10 +688,10 @@ Requesting information Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps -and between values in some error messages. Coq can also highlight differences +|Coq| can automatically highlight the differences between successive proof steps +and between values in some error messages. |Coq| can also highlight differences in the proof term. -For example, the following screenshots of CoqIDE and coqtop show the application +For example, the following screenshots of |CoqIDE| and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added to it. The second screenshot uses the "removed" option, so it shows the conclusion a @@ -714,7 +727,7 @@ new, no line of old text is shown for them. .. image:: ../_static/diffs-coqtop-on3.png :alt: coqtop with Set Diffs on -This image shows an error message with diff highlighting in CoqIDE: +This image shows an error message with diff highlighting in |CoqIDE|: .. @@ -735,21 +748,21 @@ How to enable diffs For coqtop, showing diffs can be enabled when starting coqtop with the ``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option -within Coq. You will need to provide the ``-color on|auto`` command-line option when +within |Coq|. You will need to provide the ``-color on|auto`` command-line option when you start coqtop in either case. Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment variable. See section :ref:`customization-by-environment-variables`. Diffs use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. -In CoqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` -command in CoqIDE. You can change the background colors shown for diffs from the +In |CoqIDE|, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in |CoqIDE|. You can change the background colors shown for diffs from the ``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also lets you control other attributes of the highlights, such as the foreground color, bold, italic, underline and strikeout. -As of June 2019, Proof General can also display Coq-generated proof diffs automatically. +Proof General can also display |Coq|-generated proof diffs automatically. Please see the PG documentation section "`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) for details. @@ -840,7 +853,7 @@ To show differences in the proof term: - In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. -- In CoqIDE, position the cursor on or just after a tactic to compare the proof term +- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term after the tactic with the proof term before the tactic, then select `View / Show Proof` from the menu or enter the associated key binding. Differences will be shown applying the current `Show Diffs` setting @@ -872,12 +885,17 @@ Controlling the effect of proof editing commands When turned on (it is off by default), this flag enables support for nested proofs: a new assertion command can be inserted before the current proof is - finished, in which case Coq will temporarily switch to the proof of this + finished, in which case |Coq| will temporarily switch to the proof of this *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` or :cmd:`Defined`), its statement will be made available (as if it had been - proved before starting the previous proof) and Coq will switch back to the + proved before starting the previous proof) and |Coq| will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ @@ -887,7 +905,7 @@ Controlling memory usage Prints heap usage statistics, which are values from the `stat` type of the `Gc` module described `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ - in the OCaml documentation. + in the |OCaml| documentation. The `live_words`, `heap_words` and `top_heap_words` values give the basic information. Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. @@ -902,7 +920,7 @@ to force |Coq| to optimize some of its internal data structures. .. cmd:: Optimize Heap Perform a heap compaction. This is generally an expensive operation. - See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ There is also an analogous tactic :tacn:`optimize_heap`. Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ca50a02562..cdbae8ade1 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -158,23 +158,23 @@ compatible with the rest of |Coq|, up to a few discrepancies: generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. + The following flags can be unset to make |SSR| more compatible with - parts of Coq: + parts of |Coq|: .. flag:: SsrRewrite Controls whether the incompatible rewrite syntax is enabled (the default). - Disabling the flag makes the syntax compatible with other parts of Coq. + Disabling the flag makes the syntax compatible with other parts of |Coq|. .. flag:: SsrIdents Controls whether tactics can refer to |SSR|-generated variables that are in the form _xxx_. Scripts with explicit references to such variables are fragile; they are prone to failure if the proof is later modified or - if the details of variable name generation change in future releases of Coq. + if the details of variable name generation change in future releases of |Coq|. The default is on, which gives an error message when the user tries to create such identifiers. Disabling the flag generates a warning instead, - increasing compatibility with other parts of Coq. + increasing compatibility with other parts of |Coq|. |Gallina| extensions -------------------- @@ -5724,11 +5724,11 @@ respectively. local function definition -.. tacv:: pose fix @fix_body +.. tacv:: pose fix @fix_decl local fix definition -.. tacv:: pose cofix @fix_body +.. tacv:: pose cofix @fix_decl local cofix definition diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4b1f312105..fe9a31e220 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -86,42 +86,36 @@ specified, the default selector is used. Although other selectors are available, only ``all``, ``!`` or a single natural number are valid default goal selectors. -.. _bindingslist: +.. _bindings: -Bindings list -~~~~~~~~~~~~~ +Bindings +~~~~~~~~ -Tactics that take a term as an argument may also support a bindings list +Tactics that take a term as an argument may also accept :token:`bindings` to instantiate some parameters of the term by name or position. -The general form of a term with a bindings list is -:n:`@term with @bindings_list` where :token:`bindings_list` can take two different forms: +The general form of a term with :token:`bindings` is +:n:`@term__tac with @bindings` where :token:`bindings` can take two different forms: -.. _bindings_list_grammar: + .. insertprodn bindings bindings .. prodn:: - ref ::= @ident - | @natural - bindings_list ::= {+ (@ref := @term) } - | {+ @term } - -+ In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an - :n:`@ident` or a :n:`@natural`. The references are determined according to the type of - :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the - type of :n:`@term` and the binding provides the tactic with an instance for the - parameter of this name. If :n:`@ref` is a number ``n``, it refers to - the ``n``-th non dependent premise of the :n:`@term`, as determined by the type - of :n:`@term`. + bindings ::= {+ ( {| @ident | @natural } := @term ) } + | {+ @one_term } + ++ In the first form, if an :token:`ident` is specified, it must be bound in the + type of :n:`@term` and provides the tactic with an instance for the + parameter of this name. If a :token:`natural` is specified, it refers to + the ``n``-th non dependent premise of :n:`@term__tac`. .. exn:: No such binder. :undocumented: -+ A bindings list can also be a simple list of terms :n:`{* @term}`. - In that case the references to which these terms correspond are - determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` - and :tacn:`case`, the terms have to - provide instances for all the dependent products in the type of term while in ++ In the second form, the interpretation of the :token:`one_term`\s depend on which + tactic they appear in. For :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` + and :tacn:`case`, the :token:`one_term`\s + provide instances for all the dependent products in the type of :n:`@term__tac` while in the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances - for the dependent products that are not bound in the conclusion of the type + for the dependent products that are not bound in the conclusion of :n:`@term__tac` are required. .. exn:: Not the right number of missing arguments. @@ -173,11 +167,11 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. Use these elementary patterns to specify a name: * :n:`@ident` — use the specified name -* :n:`?` — let Coq choose a name +* :n:`?` — let |Coq| choose a name * :n:`?@ident` — generate a name that begins with :n:`@ident` * :n:`_` — discard the matched part (unless it is required for another hypothesis) -* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name +* if a disjunction pattern omits a name, such as :g:`[|H2]`, |Coq| will choose a name **Splitting patterns** @@ -682,11 +676,11 @@ Applying theorems .. exn:: Not the right number of missing arguments. :undocumented: - .. tacv:: apply @term with @bindings_list + .. tacv:: apply @term with @bindings This also provides apply with values for instantiating premises. Here, variables are referred by names and non-dependent products by increasing numbers (see - :ref:`bindings list <bindingslist>`). + :ref:`bindings`). .. tacv:: apply {+, @term} @@ -747,8 +741,8 @@ Applying theorems tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply` does. - .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} - {? simple} eapply {+, @term {? with @bindings_list}} + .. tacv:: {? simple} apply {+, @term {? with @bindings}} + {? simple} eapply {+, @term {? with @bindings}} :name: simple apply; simple eapply This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`. @@ -849,7 +843,7 @@ Applying theorems .. flag:: Universal Lemma Under Conjunction - This flag, which preserves compatibility with versions of Coq prior to + This flag, which preserves compatibility with versions of |Coq| prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply … in`). .. tacn:: apply @term in @ident @@ -888,18 +882,18 @@ Applying theorems This applies each :token:`term` in sequence in :token:`ident`. - .. tacv:: apply {+, @term with @bindings_list} in @ident + .. tacv:: apply {+, @term with @bindings} in @ident This does the same but uses the bindings in each :n:`(@ident := @term)` to instantiate the parameters of the corresponding type of :token:`term` - (see :ref:`bindings list <bindingslist>`). + (see :ref:`bindings`). - .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident + .. tacv:: eapply {+, @term {? with @bindings } } in @ident This works as :tacn:`apply … in` but turns unresolved bindings into existential variables, if any, instead of failing. - .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @simple_intropattern + .. tacv:: apply {+, @term {? with @bindings } } in @ident as @simple_intropattern :name: apply … in … as This works as :tacn:`apply … in` then applies the :token:`simple_intropattern` @@ -911,8 +905,8 @@ Applying theorems only on subterms that contain no variables to instantiate and does not traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`. - .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} - {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} + .. tacv:: {? simple} apply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern} + {? simple} eapply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern} This summarizes the different syntactic variants of :n:`apply @term in @ident` and :n:`eapply @term in @ident`. @@ -938,48 +932,48 @@ Applying theorems :g:`constructor n` where ``n`` is the number of constructors of the head of the goal. - .. tacv:: constructor @natural with @bindings_list + .. tacv:: constructor @natural with @bindings Let ``c`` be the i-th constructor of :g:`I`, then - :n:`constructor i with @bindings_list` is equivalent to - :n:`intros; apply c with @bindings_list`. + :n:`constructor i with @bindings` is equivalent to + :n:`intros; apply c with @bindings`. .. warning:: - The terms in the :token:`bindings_list` are checked in the context + The terms in :token:`bindings` are checked in the context where constructor is executed and not in the context where :tacn:`apply` is executed (the introductions are not taken into account). - .. tacv:: split {? with @bindings_list } + .. tacv:: split {? with @bindings } :name: split This applies only if :g:`I` has a single constructor. It is then - equivalent to :n:`constructor 1 {? with @bindings_list }`. It is + equivalent to :n:`constructor 1 {? with @bindings }`. It is typically used in the case of a conjunction :math:`A \wedge B`. - .. tacv:: exists @bindings_list + .. tacv:: exists @bindings :name: exists This applies only if :g:`I` has a single constructor. It is then equivalent - to :n:`intros; constructor 1 with @bindings_list.` It is typically used in + to :n:`intros; constructor 1 with @bindings.` It is typically used in the case of an existential quantification :math:`\exists x, P(x).` - .. tacv:: exists {+, @bindings_list } + .. tacv:: exists {+, @bindings } - This iteratively applies :n:`exists @bindings_list`. + This iteratively applies :n:`exists @bindings`. .. exn:: Not an inductive goal with 1 constructor. :undocumented: - .. tacv:: left {? with @bindings_list } - right {? with @bindings_list } + .. tacv:: left {? with @bindings } + right {? with @bindings } :name: left; right These tactics apply only if :g:`I` has two constructors, for instance in the case of a disjunction :math:`A \vee B`. Then, they are respectively equivalent to - :n:`constructor 1 {? with @bindings_list }` and - :n:`constructor 2 {? with @bindings_list }`. + :n:`constructor 1 {? with @bindings }` and + :n:`constructor 2 {? with @bindings }`. .. exn:: Not an inductive goal with 2 constructors. :undocumented: @@ -1299,7 +1293,7 @@ Managing the local context .. tacv:: set @term {? in @goal_occurrences } This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` - but :token:`ident` is generated by Coq. + but :token:`ident` is generated by |Coq|. .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences } eset @term {? in @goal_occurrences } @@ -1344,7 +1338,7 @@ Managing the local context .. tacv:: pose @term This behaves as :n:`pose (@ident := @term)` but :token:`ident` is - generated by Coq. + generated by |Coq|. .. tacv:: epose (@ident {* @binder } := @term) epose @term @@ -1406,7 +1400,7 @@ Controlling the proof flow .. tacv:: assert @type This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is - generated by Coq. + generated by |Coq|. .. tacv:: assert @type by @tactic @@ -1486,7 +1480,7 @@ Controlling the proof flow .. tacv:: enough @type This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of - the hypothesis generated by Coq. + the hypothesis generated by |Coq|. .. tacv:: enough @type as @simple_intropattern @@ -1518,13 +1512,13 @@ Controlling the proof flow list of remaining subgoal to prove. .. tacv:: specialize (@ident {* @term}) {? as @simple_intropattern} - specialize @ident with @bindings_list {? as @simple_intropattern} + specialize @ident with @bindings {? as @simple_intropattern} :name: specialize; _ This tactic works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either - from arguments :n:`{* @term}` or from a :ref:`bindings list <bindingslist>`. + from arguments :n:`{* @term}` or from :ref:`bindings`. In the first form the application to :n:`{* @term}` can be partial. The first form is equivalent to :n:`assert (@ident := @ident {* @term})`. In the second form, instantiation elements can also be partial. In this case the @@ -1611,7 +1605,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. must have given the name explicitly (see :ref:`Existential-Variables`). .. note:: When you are referring to hypotheses which you did not name - explicitly, be aware that Coq may make a different decision on how to + explicitly, be aware that |Coq| may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. @@ -1765,9 +1759,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) between :token:`term` and the value that it takes in each of the possible cases. The name of the equation is specified by :token:`naming_intropattern` (see :tacn:`intros`), - in particular ``?`` can be used to let Coq generate a fresh name. + in particular ``?`` can be used to let |Coq| generate a fresh name. - .. tacv:: destruct @term with @bindings_list + .. tacv:: destruct @term with @bindings This behaves like :n:`destruct @term` providing explicit instances for the dependent premises of the type of :token:`term`. @@ -1781,9 +1775,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) are left as existential variables to be inferred later, in the same way as :tacn:`eapply` does. - .. tacv:: destruct @term using @term {? with @bindings_list } + .. tacv:: destruct @term using @term {? with @bindings } - This is synonym of :n:`induction @term using @term {? with @bindings_list }`. + This is synonym of :n:`induction @term using @term {? with @bindings }`. .. tacv:: destruct @term in @goal_occurrences @@ -1792,8 +1786,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) clause is an occurrence clause whose syntax and behavior is described in :ref:`occurrences sets <occurrencessets>`. - .. tacv:: destruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - edestruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + .. tacv:: destruct @term {? with @bindings } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings } } {? in @goal_occurrences } + edestruct @term {? with @bindings } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings } } {? in @goal_occurrences } These are the general forms of :tacn:`destruct` and :tacn:`edestruct`. They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, @@ -1806,15 +1800,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) recursion. It behaves as :n:`elim @term` but using a case-analysis elimination principle and not a recursive one. -.. tacv:: case @term with @bindings_list +.. tacv:: case @term with @bindings - Analogous to :n:`elim @term with @bindings_list` above. + Analogous to :n:`elim @term with @bindings` above. -.. tacv:: ecase @term {? with @bindings_list } +.. tacv:: ecase @term {? with @bindings } :name: ecase In case the type of :n:`@term` has dependent premises, or dependent premises - whose values are not inferable from the :n:`with @bindings_list` clause, + whose values are not inferable from the :n:`with @bindings` clause, :n:`ecase` turns them into existential variables to be resolved later on. .. tacv:: simple destruct @ident @@ -1906,10 +1900,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`(p`:sub:`1` :n:`, ... , p`:sub:`n` :n:`)` can be used instead of :n:`[ p`:sub:`1` :n:`... p`:sub:`n` :n:`]`. -.. tacv:: induction @term with @bindings_list +.. tacv:: induction @term with @bindings This behaves like :tacn:`induction` providing explicit instances for the - premises of the type of :n:`term` (see :ref:`bindings list <bindingslist>`). + premises of the type of :n:`term` (see :ref:`bindings`). .. tacv:: einduction @term :name: einduction @@ -1926,7 +1920,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) It does not expect the conclusion of the type of the first :n:`@term` to be inductive. -.. tacv:: induction @term using @term with @bindings_list +.. tacv:: induction @term using @term with @bindings This behaves as :tacn:`induction … using …` but also providing instances for the premises of the type of the second :n:`@term`. @@ -1954,8 +1948,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) induction y in x |- *. Show 2. -.. tacv:: induction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences - einduction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences +.. tacv:: induction @term with @bindings as @or_and_intropattern_loc using @term with @bindings in @goal_occurrences + einduction @term with @bindings as @or_and_intropattern_loc using @term with @bindings in @goal_occurrences These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the effects of the with, as, using, and in clauses. @@ -1978,11 +1972,11 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) products, the tactic tries to find an instance for which the elimination lemma applies and fails otherwise. -.. tacv:: elim @term with @bindings_list +.. tacv:: elim @term with @bindings :name: elim … with Allows to give explicit instances to the premises of the type of :n:`@term` - (see :ref:`bindings list <bindingslist>`). + (see :ref:`bindings`). .. tacv:: eelim @term :name: eelim @@ -1991,15 +1985,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) existential variables to be resolved later on. .. tacv:: elim @term using @term - elim @term using @term with @bindings_list + elim @term using @term with @bindings Allows the user to give explicitly an induction principle :n:`@term` that is not the standard one for the underlying inductive type of :n:`@term`. The - :n:`@bindings_list` clause allows instantiating premises of the type of + :n:`@bindings` clause allows instantiating premises of the type of :n:`@term`. -.. tacv:: elim @term with @bindings_list using @term with @bindings_list - eelim @term with @bindings_list using @term with @bindings_list +.. tacv:: elim @term with @bindings using @term with @bindings + eelim @term with @bindings using @term with @bindings These are the most general forms of :tacn:`elim` and :tacn:`eelim`. It combines the effects of the ``using`` clause and of the two uses of the ``with`` clause. @@ -2148,13 +2142,13 @@ and an explanation of the underlying technique. :n:`discriminate @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. -.. tacv:: discriminate @term with @bindings_list +.. tacv:: discriminate @term with @bindings This does the same thing as :n:`discriminate @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. .. tacv:: ediscriminate @natural - ediscriminate @term {? with @bindings_list} + ediscriminate @term {? with @bindings} :name: ediscriminate; _ This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the @@ -2212,7 +2206,7 @@ and an explanation of the underlying technique. different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and :g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and :g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable - equality has been declared using the command :cmd:`Scheme Equality` + equality has been declared using :cmd:`Scheme` :n:`Equality ...` (see :ref:`proofschemes-induction-principles`), the use of a sigma type is avoided. @@ -2237,13 +2231,13 @@ and an explanation of the underlying technique. :n:`injection @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. - .. tacv:: injection @term with @bindings_list + .. tacv:: injection @term with @bindings This does the same as :n:`injection @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. .. tacv:: einjection @natural - einjection @term {? with @bindings_list} + einjection @term {? with @bindings} :name: einjection; _ This works the same as :n:`injection` but if the type of :n:`@term`, or the @@ -2258,10 +2252,10 @@ and an explanation of the underlying technique. .. exn:: goal does not satisfy the expected preconditions. :undocumented: - .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} + .. tacv:: injection @term {? with @bindings} as {+ @simple_intropattern} injection @natural as {+ @simple_intropattern} injection as {+ @simple_intropattern} - einjection @term {? with @bindings_list} as {+ @simple_intropattern} + einjection @term {? with @bindings} as {+ @simple_intropattern} einjection @natural as {+ @simple_intropattern} einjection as {+ @simple_intropattern} @@ -2273,10 +2267,10 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. - .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern + .. tacv:: injection @term {? with @bindings} as @injection_intropattern injection @natural as @injection_intropattern injection as @injection_intropattern - einjection @term {? with @bindings_list} as @injection_intropattern + einjection @term {? with @bindings} as @injection_intropattern einjection @natural as @injection_intropattern einjection as @injection_intropattern @@ -2359,7 +2353,7 @@ and an explanation of the underlying technique. ``inversion`` generally behaves in a slightly more expectable way than ``inversion`` (no artificial duplication of some hypotheses referring to other hypotheses). To take benefit of these improvements, it is enough to use - ``inversion ... as []``, letting the names being finally chosen by Coq. + ``inversion ... as []``, letting the names being finally chosen by |Coq|. .. example:: @@ -3029,7 +3023,7 @@ the conversion in hypotheses :n:`{+ @ident}`. These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In - correspondence with the kinds of reduction considered in Coq namely + correspondence with the kinds of reduction considered in |Coq| namely :math:`\beta` (reduction of functional application), :math:`\delta` (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), :math:`\iota` (reduction of @@ -3111,8 +3105,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: native_compute :name: native_compute - This tactic evaluates the goal by compilation to OCaml as described - in :cite:`FullReduction`. If Coq is running in native code, it can be + This tactic evaluates the goal by compilation to |OCaml| as described + in :cite:`FullReduction`. If |Coq| is running in native code, it can be typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive computations. @@ -4024,14 +4018,14 @@ automatically created. ``typeclass_instances`` hint database. -Hint databases defined in the Coq standard library -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Hint databases defined in the |Coq| standard library +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Several hint databases are defined in the Coq standard library. The +Several hint databases are defined in the |Coq| standard library. The actual content of a database is the collection of hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules may extend the database. -At Coq startup, only the core database is nonempty and can be used. +At |Coq| startup, only the core database is nonempty and can be used. :core: This special database is automatically used by ``auto``, except when pseudo-database ``nocore`` is given to ``auto``. The core database @@ -4124,7 +4118,7 @@ use one or several databases specific to your development. Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in the bases :n:`{+ @ident}`. -.. cmd:: Hint Rewrite {+ @term} using @tactic : {+ @ident} +.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the tactic ``tactic`` will be applied to the generated subgoals, the main subgoal @@ -4152,7 +4146,7 @@ but this is a mere workaround and has some limitations (for instance, external hints cannot be removed). A proper way to fix this issue is to bind the hints to their module scope, as -for most of the other objects Coq uses. Hints should only be made available when +for most of the other objects |Coq| uses. Hints should only be made available when the module they are defined in is imported, not just required. It is very difficult to change the historical behavior, as it would break a lot of scripts. We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` @@ -4408,7 +4402,7 @@ some incompatibilities. .. exn:: I don’t know how to handle dependent equality. The decision procedure managed to find a proof of the goal or of a - discriminable equality but this proof could not be built in Coq because of + discriminable equality but this proof could not be built in |Coq| because of dependently-typed functions. .. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. @@ -4600,13 +4594,13 @@ symbol :g:`=`. :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. -.. tacv:: simplify_eq @term with @bindings_list +.. tacv:: simplify_eq @term with @bindings This does the same as :n:`simplify_eq @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. .. tacv:: esimplify_eq @natural - esimplify_eq @term {? with @bindings_list} + esimplify_eq @term {? with @bindings} :name: esimplify_eq; _ This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the @@ -4855,14 +4849,14 @@ Proof maintenance *Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps -may explicitly refer to these names. However, future versions of Coq may not assign +may explicitly refer to these names. However, future versions of |Coq| may not assign names exactly the same way, which could cause the proof to fail because the new names don't match the explicit references in the proof. The following "Mangle Names" settings let users find all the places where proofs rely on automatically generated names, which can then be named explicitly to avoid any incompatibility. These -settings cause Coq to generate different names, producing errors for +settings cause |Coq| to generate different names, producing errors for references to automatically generated names. .. flag:: Mangle Names @@ -4884,7 +4878,7 @@ Performance-oriented tactic variants For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization, it skips checking that :n:`@term` is convertible to the goal. - Recall that the Coq kernel typechecks proofs again when they are concluded to + Recall that the |Coq| kernel typechecks proofs again when they are concluded to ensure safety. Hence, using :tacn:`change` checks convertibility twice overall, while :tacn:`change_no_check` can produce ill-typed terms, but checks convertibility only once. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 6c07253bce..301559d69d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -637,10 +637,10 @@ file is a particular case of a module called a *library file*. .. cmd:: Declare ML Module {+ @string } - This commands dynamically loads OCaml compiled code from + This commands dynamically loads |OCaml| compiled code from a :n:`.mllib` file. It is used to load plugins dynamically. The - files must be accessible in the current OCaml loadpath (see the + files must be accessible in the current |OCaml| loadpath (see the command :cmd:`Add ML Path`). The :n:`.mllib` suffix may be omitted. This command is reserved for plugin developers, who should provide @@ -656,7 +656,7 @@ file is a particular case of a module called a *library file*. .. cmd:: Print ML Modules - This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. + This prints the name of all |OCaml| modules loaded with :cmd:`Declare ML Module`. To know from where these module were loaded, the user should use the command :cmd:`Locate File`. @@ -719,13 +719,13 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Add ML Path @string - This command adds the path :n:`@string` to the current OCaml + This command adds the path :n:`@string` to the current |OCaml| loadpath (cf. :cmd:`Declare ML Module`). .. cmd:: Print ML Path - This command displays the current OCaml loadpath. This + This command displays the current |OCaml| loadpath. This command makes sense only under the bytecode version of ``coqtop``, i.e. using option ``-byte`` (cf. :cmd:`Declare ML Module`). @@ -794,10 +794,10 @@ Quitting and debugging .. cmd:: Drop - This command temporarily enters the OCaml toplevel. + This command temporarily enters the |OCaml| toplevel. It is a debug facility used by |Coq|’s implementers. Valid only in the bytecode version of coqtop. - The OCaml command: + The |OCaml| command: :: @@ -980,7 +980,7 @@ described first. This command has an effect on unfoldable constants, i.e. on constants defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command - assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc, + associated with a definition such as :cmd:`Fixpoint`, etc, or by a proof ended by :cmd:`Defined`. The command tells not to unfold the constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding a constant is replacing it by its definition). @@ -1230,15 +1230,15 @@ in support libraries of plug-ins. .. _exposing-constants-to-ocaml-libraries: -Exposing constants to OCaml libraries -````````````````````````````````````` +Exposing constants to |OCaml| libraries +``````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 - Makes the constant :n:`@qualid__1` accessible to OCaml libraries under + Makes the constant :n:`@qualid__1` accessible to |OCaml| libraries under the name :n:`@qualid__2`. The constant can then be dynamically located - in OCaml code by - calling :n:`Coqlib.lib_ref "@qualid__2"`. The OCaml code doesn't need + in |OCaml| code by + calling :n:`Coqlib.lib_ref "@qualid__2"`. The |OCaml| code doesn't need to know where the constant is defined (what file, module, library, etc.). As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, @@ -1267,7 +1267,7 @@ Registering primitive operations .. cmd:: Primitive @ident_decl {? : @term } := #@ident - Makes the primitive type or primitive operator :n:`#@ident` defined in OCaml + Makes the primitive type or primitive operator :n:`#@ident` defined in |OCaml| accessible in |Coq| commands and tactics. For internal use by implementors of |Coq|'s standard library or standard library replacements. No space is allowed after the `#`. Invalid values give a syntax |