Doc: replace "coqfoo" with "rocq foo"

doc/sphinx/changes.rst

@@ -2238,7 +2238,7 @@ Command-line tools
   ``coq_makefile`` when compiling OCaml code, since
   it is no longer required by Coq. To re-enable passing
   the flag, put ``CAMLFLAGS+=-rectypes`` in the local makefile,
-  e.g., ``CoqMakefile.local`` (see :ref:`coqmakefilelocal`)
+  e.g., ``CoqMakefile.local`` (see :ref:`rocqmakefilelocal`)
   (`#17038 <https://github.com/coq/coq/pull/17038>`_,
   by Karl Palmskog with help from Gaëtan Gilbert).
 - **Changed:**
@@ -4509,7 +4509,7 @@ Command-line tools
   by Emilio Jesus Gallego Arias).
 - **Changed:**
   Syntax of `_CoqProject` files: `-arg` is now handled by :ref:`coq_makefile
-  <coq_makefile>` and not by `make`. Unquoted `#` now start line comments
+  <rocq_makefile>` and not by `make`. Unquoted `#` now start line comments
   (`#14558 <https://github.com/coq/coq/pull/14558>`_,
   by Stéphane Desarzens, with help from Jim Fehrle and Enrico Tassi).
 - **Changed:**
@@ -4529,13 +4529,13 @@ Command-line tools
   (`#14957 <https://github.com/coq/coq/pull/14957>`_,
   by Gaëtan Gilbert)
 - **Removed:**
-  These options of :ref:`coq_makefile <coq_makefile>`: `-extra`, `-extra-phony`,
+  These options of :ref:`coq_makefile <rocq_makefile>`: `-extra`, `-extra-phony`,
   `-custom`, `-no-install`, `-install`, `-no-opt`, `-byte`.
   Support for subdirectories is also removed
   (`#14558 <https://github.com/coq/coq/pull/14558>`_,
   by Stéphane Desarzens, with help from Jim Fehrle and Enrico Tassi).
 - **Added:**
-  :ref:`coq_makefile <coq_makefile>` now takes the `-docroot` option as alternative to the
+  :ref:`coq_makefile <rocq_makefile>` now takes the `-docroot` option as alternative to the
   `INSTALLCOQDOCROOT` variable
   (`#14558 <https://github.com/coq/coq/pull/14558>`_,
   by Stéphane Desarzens, with help from Jim Fehrle and Enrico Tassi).
@@ -5457,14 +5457,14 @@ Native Compilation
   by Pierre-Marie Pédrot).
 - **Deprecated:**
   the `-native-compiler` option for coqc. It is now recommended
-  to use the :ref:`coqnative` binary instead to generate native
+  to use the :ref:`rocqnative` binary instead to generate native
   compilation files ahead of time
   (`#14309 <https://github.com/coq/coq/pull/14309>`_,
   by Pierre-Marie Pédrot).
 - **Added:**
   A standalone `coqnative` binary that performs native compilation
   out of `vo` files, allowing to split library compilation from
-  native compilation. See :ref:`coqnative`. The hybrid build
+  native compilation. See :ref:`rocqnative`. The hybrid build
   system was adapted to perform a split compilation on the stdlib
   (`#13287 <https://github.com/coq/coq/pull/13287>`_,
   by Pierre-Marie Pédrot).
@@ -6322,7 +6322,7 @@ Tools
 - **Changed:**
   Added the ability for coq_makefile to directly set the installation folders,
   through the `COQLIBINSTALL` and `COQDOCINSTALL` variables.
-  See :ref:`coqmakefilelocal`
+  See :ref:`rocqmakefilelocal`
   (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi).
 - **Removed:** The option ``-I`` of coqchk was removed (it was
   deprecated in Coq 8.8) (`#12613
@@ -7177,7 +7177,7 @@ Tools
   <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
 - **Added:**
   A new documentation environment ``details`` to make certain portion
-  of a Coq document foldable.  See :ref:`coqdoc-hide-show`
+  of a Coq document foldable.  See :ref:`rocqdoc-hide-show`
   (`#10592 <https://github.com/coq/coq/pull/10592>`_,
   by Thomas Letan).
 - **Added:**

doc/sphinx/history.rst

@@ -675,7 +675,7 @@ new extraction procedure, unlike the one implemented in previous version
 of Coq is able to handle all terms in the Calculus of Inductive
 Constructions, even involving universes and strong elimination. P.
 Letouzey adapted user contributions to extract ML programs when it was
-sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation
+sensible. Jean-Christophe Filliâtre wrote ``coqdoc`` (now ``rocq doc``), a documentation
 tool for Coq libraries usable from version 7.2.
 
 Bruno Barras improved the efficiency of the reduction algorithm and the

doc/sphinx/language/cic.rst

@@ -434,7 +434,7 @@ The Calculus of Inductive Constructions with impredicative Set
 
 The Rocq Prover can be used as a type checker for the Calculus of Inductive
 Constructions with an impredicative sort :math:`\Set` by using the compiler
-option ``-impredicative-set``. For example, using the ordinary `coqtop`
+option ``-impredicative-set``. For example, using the ordinary `rocq repl`
 command, the following is rejected,
 
 .. example::
@@ -443,7 +443,7 @@ command, the following is rejected,
 
       Fail Definition id: Set := forall X:Set,X->X.
 
-while it will type check, if one uses instead the `coqtop`
+while it will type check, if one uses instead the `rocq repl`
 ``-impredicative-set`` option..
 
 The major change in the theory concerns the rule for product formation

doc/sphinx/language/core/basic.rst

@@ -510,8 +510,8 @@ Document-level attributes
    :name: Attributes
 
    Associates attributes with the
-   document. When compiled with ``coqc`` (see Section
-   :ref:`thecoqcommands`), the attributes are associated with the
+   document. When compiled with ``rocq c`` (see Section
+   :ref:`therocqcommands`), the attributes are associated with the
    compiled file and may have an effect when the file is loaded with
    :cmd:`Require`. Supported attributes include :attr:`deprecated`
    and :attr:`warn`.

doc/sphinx/language/core/modules.rst

@@ -566,7 +566,7 @@ as :n:`Stdlib.Init.Logic`, in which:
   corresponds to the file system path :n:`Init/Logic.v` on Linux)
 
 When Rocq is processing a script that hasn't been saved in a file, such as a new
-buffer in CoqIDE or anything in coqtop, definitions in the script are associated
+buffer in CoqIDE or anything in `rocq repl`, definitions in the script are associated
 with the logical name :n:`Top` and there is no associated file system path.
 
 **Item part.** Items are further qualified by a suffix in the form