diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 37 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 9 |
6 files changed, 33 insertions, 35 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 64d4eddf0..1d3b66173 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -305,6 +305,8 @@ explicitations (as for terms 2.7.11). end). +.. _matching-dependent: + Matching objects of dependent types ----------------------------------- @@ -414,6 +416,7 @@ length, by writing I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. +.. _match-in-patterns: Patterns in ``in`` ~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 0e72c996f..d60387f4f 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -707,20 +707,18 @@ instances are tried at each node of the search tree). To speed it up, declare your constant as rigid for proof search using the command ``Typeclasses Opaque`` (see :ref:`TypeclassesTransparent`). - Strategies for rewriting ------------------------ - Definitions ~~~~~~~~~~~ -The generalized rewriting tactic is based on a set of strategies that -can be combined to obtain custom rewriting procedures. Its set of -strategies is based on Elan’s rewriting strategies :ref:`TODO-102-biblio`. Rewriting +The generalized rewriting tactic is based on a set of strategies that can be +combined to obtain custom rewriting procedures. Its set of strategies is based +on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a -strategy expression. Strategies are defined inductively as described -by the following grammar: +strategy expression. Strategies are defined inductively as described by the +following grammar: .. productionlist:: rewriting s, t, u : `strategy` diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 68e071d7c..ec1b942e0 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -272,25 +272,24 @@ Activating the Printing of Coercions Classes as Records ------------------ -We allow the definition of *Structures with Inheritance* (or -classes as records) by extending the existing ``Record`` macro -(see Section :ref:`record-types`). Its new syntax is: - -.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. - - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` - are their respective types. If ``:>`` is used instead of ``:`` in - the declaration of a field, then the name of this field is automatically - declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform - inheritance condition. If the optional ``>`` is given before the - record name, then the constructor name is automatically declared as - a coercion from the class of the last field type to the record name - (this may fail if the uniform inheritance condition is not - satisfied). +We allow the definition of *Structures with Inheritance* (or classes as records) +by extending the existing :cmd:`Record` macro. Its new syntax is: + +.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. + + The first identifier `ident` is the name of the defined record and + `sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be ``Build_``\ `ident` if not given). + The other identifiers are the names of the fields, and the `term` + are their respective types. If ``:>`` is used instead of ``:`` in + the declaration of a field, then the name of this field is automatically + declared as a coercion from the record name to the class of this + field type. Remark that the fields always verify the uniform + inheritance condition. If the optional ``>`` is given before the + record name, then the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). .. note:: diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a2940881d..1c3fdeb43 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,8 +135,7 @@ support types, avoiding uses of proof-irrelevance that would come up when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts -Definition (see Section :ref:`gallina_def`) and Fixpoint -(see Section :ref:`TODO-1.3.4-Fixpoint`) +:cmd:`Definition` and :cmd:`Fixpoint` in that they define constants. However, they may require the user to prove some goals to construct the final definitions. @@ -197,7 +196,7 @@ The optional order annotation follows the grammar: + :g:`wf R x` which is equivalent to :g:`measure x (R)`. The structural fixpoint operator behaves just like the one of |Coq| (see -Section :ref:`TODO-1.3.4-Fixpoint`), except it may also generate obligations. It works +:cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. .. coqtop:: reset none diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index b861892cb..ae666a0d4 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -701,7 +701,7 @@ for |Coq|’s type-checker. Let us see why: At each step of rewriting, the whole context is duplicated in the proof term. Then, a tactic that does hundreds of rewriting generates huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote -it using reflection (see his article in TACS’97 [Bou97]_). Later, it +it using reflection (see :cite:`Bou97`). Later, it was rewritten by Patrick Loiseleur: the new tactic does not any more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not only to replace the rewriting steps, but also to achieve the diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index add03b946..8861cac8a 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -148,11 +148,10 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we -provide a new way to introduce variables into section contexts, -compatible with the implicit argument mechanism. The new command works -similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it -accepts any binding context as argument. For example: +To ease the parametrization of developments by type classes, we provide a new +way to introduce variables into section contexts, compatible with the implicit +argument mechanism. The new command works similarly to the :cmd:`Variables` +vernacular, except it accepts any binding context as argument. For example: .. coqtop:: all |