Apply Coq -> Rocq renaming in documentation files

Author: mattam82

.gitignore

@@ -166,3 +166,5 @@ user-contrib/Ltac2/dune
 
 .wrappers
 rocq-stdlib-doc.opam
+doc/stdlib/Library.fdb_latexmk
+doc/stdlib/Library.fls

doc/common/macros.tex

@@ -91,6 +91,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%
 
 \newcommand{\Coq}{\textsc{Coq}}
+\newcommand{\Rocq}{\textsc{Rocq}}
 \newcommand{\gallina}{\textsc{Gallina}}
 \newcommand{\Gallina}{\textsc{Gallina}}
 \newcommand{\CoqIDE}{\textsc{CoqIDE}}

doc/sphinx/introduction.rst

@@ -1,5 +1,5 @@
-The is the reference manual of the Standard Library of Coq.
-It mostly presents a few tactics.
+This is the reference manual of the Standard Library of the Rocq Prover.
+It mostly presents a few notations and tactics.
 
 .. only:: html
 

doc/sphinx/language/coq-library.rst

@@ -29,8 +29,8 @@ These directories belong to the initial load path of the system, and
 the modules they provide are compiled at installation time. So they
 are directly accessible with the command ``Require``.
 
-The different modules of the Coq standard library are documented
-online at https://coq.inria.fr/stdlib/.
+The different modules of the Rocq standard library are documented
+online at https://rocq-prover.org/stdlib/.
 
 Peano’s arithmetic (nat)
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -250,7 +250,7 @@ Floats library
 ~~~~~~~~~~~~~~
 
 The standard library has a small ``Floats`` module for accessing
-processor floating-point operations through the Coq kernel.
+processor floating-point operations through the Rocq kernel.
 However, while this module supports computation and has a bit-level
 specification, it doesn't include elaborate theorems, such as a link
 to real arithmetic or various error bounds. To do proofs by

doc/stdlib/Library.tex

@@ -23,9 +23,9 @@
 \tableofcontents
 
 \newpage
-% \section*{The \Coq\ standard library}
+% \section*{The \Rocq\ standard library}
 
-This document is a short description of the \Coq\ standard library.
+This document is a short description of the \Rocq\ standard library.
 This library comes with the system as a complement of the core library
 (the {\bf Init} library ; see the Reference Manual for a description
 of this library). It provides a set of modules directly available