diff options
| author | Maxime Dénès | 2017-12-18 10:51:02 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 10:51:02 +0100 |
| commit | f27fa07029475f2366e101cff7bc895aac415b67 (patch) | |
| tree | 7f93595dca090c530318dddcc7ded838d073775d | |
| parent | 32acb87d4b6b53b26a891b93df6244e0446411b0 (diff) | |
| parent | 60f2af7b2d3f130c02250807df33a07c2024d808 (diff) | |
Merge PR #6453: [doc] Nit on the manual.
| -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 |