diff options
Diffstat (limited to 'doc/sphinx/addendum/ring.rst')
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index b861892cb..47d3a7d7c 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -171,21 +171,21 @@ performs the simplification in the hypothesis named :n:`@ident`. Error messages: -.. exn:: not a valid ring equation +.. exn:: Not a valid ring equation. The conclusion of the goal is not provable in the corresponding ring theory. -.. exn:: arguments of ring_simplify do not have all the same type +.. exn:: Arguments of ring_simplify do not have all the same type. ``ring_simplify`` cannot simplify terms of several rings at the same time. Invoke the tactic once per ring structure. -.. exn:: cannot find a declared ring structure over @term +.. exn:: Cannot find a declared ring structure over @term. No ring has been declared for the type of the terms to be simplified. Use ``Add Ring`` first. -.. exn:: cannot find a declared ring structure for equality @term +.. exn:: Cannot find a declared ring structure for equality @term. Same as above is the case of the ``ring`` tactic. @@ -303,7 +303,7 @@ following property: The syntax for adding a new ring is -.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}. +.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} The :n:`@ident` is not relevant. It is just used for error messages. The :n:`@term` is a proof that the ring signature satisfies the (semi-)ring @@ -396,18 +396,18 @@ div :n:`@term` Error messages: -.. exn:: bad ring structure +.. exn:: Bad ring structure. The proof of the ring structure provided is not of the expected type. -.. exn:: bad lemma for decidability of equality +.. exn:: Bad lemma for decidability of equality. The equality function provided in the case of a computational ring has not the expected type. -.. exn:: ring operation should be declared as a morphism +.. exn:: Ring operation should be declared as a morphism. A setoid associated to the carrier of the ring structure has been found, but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`. @@ -656,7 +656,7 @@ zero for the correctness of the algorithm. The syntax for adding a new field is -.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}. +.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} The :n:`@ident` is not relevant. It is just used for error messages. :n:`@term` is a proof that the field signature satisfies the @@ -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 |