Doc: rename coqtop:: -> rocqtop::, coqdoc:: -> rocqdoc::

The implementation is unchanged, ie it's still called coqdomain, calls coqtop, produces CSS classes named coqdoc-keyword etc
SkySkimmer · Dec 13, 2024 · 9a6946d · 9a6946d
1 parent e2dc7ac
commit 9a6946d
Show file tree

Hide file tree

Showing 50 changed files with 1,383 additions and 1,383 deletions.
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
@@ -223,16 +223,16 @@ Coq directives
 
 In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives:
 
-``.. coqtop::`` A reST directive to describe interactions with Coqtop.
+``.. rocqtop::`` A reST directive to describe interactions with Coqtop.
     Usage::
 
-       .. coqtop:: options…
+       .. rocqtop:: options…
 
           Coq code to send to coqtop
 
     Example::
 
-       .. coqtop:: in reset
+       .. rocqtop:: in reset
 
           Print nat.
           Definition a := 1.
@@ -261,20 +261,20 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
         Be careful when using it to surround the code block with a sentence explaining what
         extra requirement is needed to compile it.
 
-    ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+    ``coqtop``\ 's state is preserved across consecutive ``.. rocqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
     reST source file).  Use the ``reset`` option to reset Coq's state.
 
-``.. coqdoc::`` A reST directive to display Coqtop-formatted source code.
+``.. rocqdoc::`` A reST directive to display Coqtop-formatted source code.
     Usage::
 
-       .. coqdoc::
+       .. rocqdoc::
 
           Coq code to highlight
 
     Example::
 
-       .. coqdoc::
+       .. rocqdoc::
 
           Definition test := 1.
 
@@ -292,7 +292,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
 
           The following adds ``plus_comm`` to the ``plu`` database:
 
-          .. coqdoc::
+          .. rocqdoc::
 
              Hint Resolve plus_comm : plu.
 
@@ -455,21 +455,21 @@ DON'T
 
      .. tacv:: assert form as simple_intropattern
 
-Using the ``.. coqtop::`` directive for syntax highlighting
+Using the ``.. rocqtop::`` directive for syntax highlighting
 -----------------------------------------------------------
 
 DO
   .. code::
 
      A tactic of the form:
 
-     .. coqdoc::
+     .. rocqdoc::
 
         do [ t1 | … | tn ].
 
      is equivalent to the standard Ltac expression:
 
-     .. coqdoc::
+     .. rocqdoc::
 
         first [ t1 | … | tn ].
 
@@ -478,13 +478,13 @@ DON'T
 
      A tactic of the form:
 
-     .. coqtop:: in
+     .. rocqtop:: in
 
         do [ t1 | … | tn ].
 
      is equivalent to the standard Ltac expression:
 
-     .. coqtop:: in
+     .. rocqtop:: in
 
         first [ t1 | … | tn ].
 
@@ -513,7 +513,7 @@ DO
 
      Here is a useful axiom:
 
-     .. coqdoc::
+     .. rocqdoc::
 
         Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
 
@@ -531,7 +531,7 @@ DON'T
 
      .. example::
 
-        .. coqdoc::
+        .. rocqdoc::
 
            Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
 
@@ -541,13 +541,13 @@ Tips and tricks
 Nested lemmas
 -------------
 
-The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
+The ``.. rocqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
 
-   .. coqtop:: all
+   .. rocqtop:: all
 
       Lemma l1: 1 + 1 = 2.
 
-   .. coqtop:: all
+   .. rocqtop:: all
 
       Lemma l2: 2 + 2 <> 1.
 

diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
@@ -190,21 +190,21 @@ DON'T
 
      .. tacv:: assert form as simple_intropattern
 
-Using the ``.. coqtop::`` directive for syntax highlighting
+Using the ``.. rocqtop::`` directive for syntax highlighting
 -----------------------------------------------------------
 
 DO
   .. code::
 
      A tactic of the form:
 
-     .. coqdoc::
+     .. rocqdoc::
 
         do [ t1 | … | tn ].
 
      is equivalent to the standard Ltac expression:
 
-     .. coqdoc::
+     .. rocqdoc::
 
         first [ t1 | … | tn ].
 
@@ -213,13 +213,13 @@ DON'T
 
      A tactic of the form:
 
-     .. coqtop:: in
+     .. rocqtop:: in
 
         do [ t1 | … | tn ].
 
      is equivalent to the standard Ltac expression:
 
-     .. coqtop:: in
+     .. rocqtop:: in
 
         first [ t1 | … | tn ].
 
@@ -248,7 +248,7 @@ DO
 
      Here is a useful axiom:
 
-     .. coqdoc::
+     .. rocqdoc::
 
         Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
 
@@ -266,7 +266,7 @@ DON'T
 
      .. example::
 
-        .. coqdoc::
+        .. rocqdoc::
 
            Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
 
@@ -276,13 +276,13 @@ Tips and tricks
 Nested lemmas
 -------------
 
-The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
+The ``.. rocqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
 
-   .. coqtop:: all
+   .. rocqtop:: all
 
       Lemma l1: 1 + 1 = 2.
 
-   .. coqtop:: all
+   .. rocqtop:: all
 
       Lemma l2: 2 + 2 <> 1.
 

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
@@ -18,7 +18,7 @@ to any of the three.
    the extraction framework should first be loaded explicitly
    via ``From Corelib Require Extraction``.
 
-.. coqtop:: in
+.. rocqtop:: in
 
    From Corelib Require Extraction.
 
@@ -294,7 +294,7 @@ what ML term corresponds to a given axiom.
 
      The number of type variables is checked by the system. For example:
 
-     .. coqtop:: in
+     .. rocqtop:: in
 
         Axiom Y : Set -> Set -> Set.
         Extract Constant Y "'a" "'b" => " 'a * 'b ".
@@ -303,7 +303,7 @@ what ML term corresponds to a given axiom.
       The extraction recognizes whether the realized axiom
       should become a ML type constant or a ML object declaration. For example:
 
-      .. coqtop:: in
+      .. rocqtop:: in
 
          Axiom X:Set.
          Axiom x:X.
@@ -404,7 +404,7 @@ native boolean type instead of the Rocq one. The syntax is the following:
 
 Typical examples are the following:
 
-.. coqtop:: in
+.. rocqtop:: in
 
    Extract Inductive unit => "unit" [ "()" ].
    Extract Inductive bool => "bool" [ "true" "false" ].
@@ -417,15 +417,15 @@ Typical examples are the following:
    OCaml's lexical criteria for an infix symbol, then the rest of the string is
    used as an infix constructor or type.
 
-.. coqtop:: in
+.. rocqtop:: in
 
    Extract Inductive list => "list" [ "[]" "(::)" ].
    Extract Inductive prod => "(*)"  [ "(,)" ].
 
 As an example of translation to a non-inductive datatype, let's turn
 ``nat`` into OCaml ``int`` (see caveat above):
 
-.. coqtop:: in
+.. rocqtop:: in
 
    Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
 
@@ -448,7 +448,7 @@ OCaml code with C code, the linker needs to know
 
    For example:
 
-   .. coqtop:: in
+   .. rocqtop:: in
 
       From Corelib Require Extraction.
       Extract Inductive nat => int [ "0" "Stdlib.Int.succ" ].
@@ -629,7 +629,7 @@ alright but the generated code may be refused by the ML
 type checker. A very well known example is the ``distr-pair``
 function:
 
-.. coqtop:: in
+.. rocqtop:: in
 
    Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y).
 
@@ -651,7 +651,7 @@ Secondly, some Rocq definitions may have no counterpart in ML. This
 happens when there is a quantification over types inside the type
 of a constructor; for example:
 
-.. coqtop:: in
+.. rocqtop:: in
 
    Inductive anything : Type := dummy : forall A:Set, A -> anything.
 
@@ -698,7 +698,7 @@ where ``diveucl`` is a type for the pair of the quotient and the
 modulo, plus some logical assertions that disappear during extraction.
 We can now extract this program to OCaml:
 
-.. coqtop:: reset all extra
+.. rocqtop:: reset all extra
 
    From Corelib Require Extraction.
    From Stdlib Require Import Euclid Wf_nat.