diff options
| author | Emilio Jesus Gallego Arias | 2017-12-17 09:04:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-17 09:05:28 +0100 |
| commit | 60f2af7b2d3f130c02250807df33a07c2024d808 (patch) | |
| tree | e371414d18ef5479aa1c4b01e02ebcd811958b2f | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
[doc] Nit on the manual.
`ssrnat` is mentioned, but it is not distributed with Coq.
| -rw-r--r-- | doc/refman/RefMan-ssr.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index be199e0b24..31dabcdd4e 100644 --- a/doc/refman/RefMan-ssr.tex +++ b/doc/refman/RefMan-ssr.tex @@ -3096,10 +3096,10 @@ the tactic \ssrC{rewrite (=~ multi1)} is equivalent to \end{lstlisting} except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created. -Rewriting with multirules -is useful to implement simplification or transformation -procedures, to be applied on terms of small to medium size. For -instance the library \ssrL{ssrnat} provides two implementations for +Rewriting with multirules is useful to implement simplification or +transformation procedures, to be applied on terms of small to medium +size. For instance, the library \ssrL{ssrnat} --- available in the +external math-comp library --- provides two implementations for arithmetic operations on natural numbers: an elementary one and a tail recursive version, less inefficient but also less convenient for reasoning purposes. The library also provides one lemma per such |