From 60f2af7b2d3f130c02250807df33a07c2024d808 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 17 Dec 2017 09:04:35 +0100
Subject: [doc] Nit on the manual.

`ssrnat` is mentioned, but it is not distributed with Coq.
---
 doc/refman/RefMan-ssr.tex | 8 ++++----
 1 file 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
-- 
cgit v1.2.3