diff --git a/.github/workflows/ci-macos.yml b/.github/workflows/ci-macos.yml
index 728de341ad53b..013285241604d 100644
--- a/.github/workflows/ci-macos.yml
+++ b/.github/workflows/ci-macos.yml
@@ -36,7 +36,7 @@ jobs:
           eval $(opam env)
           ./configure -prefix "$(pwd)/_install_ci" -native-compiler no
           make dunestrap
-          dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,coqide
+          dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,rocqide
         env:
           MACOSX_DEPLOYMENT_TARGET: "10.11"
           NJOBS: "2"
@@ -44,7 +44,7 @@ jobs:
       - name: Install Coq
         run: |
           eval $(opam env)
-          dune install --prefix="$(pwd)/_install_ci" rocq-runtime coq-core rocq-core coqide-server coqide
+          dune install --prefix="$(pwd)/_install_ci" rocq-runtime coq-core rocq-core coqide-server rocqide
 
       - name: Run Coq Test Suite
         run: |
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ddef3ca83ed7e..8511acf5b0359 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -70,7 +70,7 @@ before_script:
   interruptible: true
   extends: .auto-use-tags
   variables:
-    COQIDE: "opt"
+    ROCQIDE: "opt"
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
@@ -86,7 +86,7 @@ before_script:
     - cp dev/ci/dune-workspace.ci dune-workspace
 
     - PKGS=rocq-runtime,coq-core,rocq-core,coqide-server
-    - if [ "$COQIDE" != "no" ]; then PKGS=${PKGS},coqide; fi
+    - if [ "$ROCQIDE" != "no" ]; then PKGS=${PKGS},rocqide; fi
     - dev/ci/gitlab-section.sh start coq.clean coq.clean
     - make clean # ensure that `make clean` works on a fresh clone
     - dev/ci/gitlab-section.sh end coq.clean
@@ -115,7 +115,7 @@ before_script:
     - make $DUNE_TARGET
     - tar cfj _build.tar.bz2 _build
   variables:
-    DUNE_TARGET: "world coqide"
+    DUNE_TARGET: "world rocqide"
   artifacts:
     name: "$CI_JOB_NAME"
     when: always
@@ -249,7 +249,7 @@ before_script:
     - if command -v coqc; then exit 1; fi # coq-core didn't get autoinstalled
     - opam pin add --kind=path coq-core.dev .
     - opam pin add --kind=path coqide-server.dev .
-    - opam pin add --kind=path coqide.dev .
+    - opam pin add --kind=path rocqide.dev .
   after_script:
     - eval $(opam env)
     - du -ha "$(coqc -where)" > files.listing
@@ -315,13 +315,13 @@ build:base:
     COQ_EXTRA_CONF: "-native-compiler yes"
   only: *full-ci
 
-# no coqide for 32bit: libgtk installation problems
+# no rocqide for 32bit: libgtk installation problems
 build:base+32bit:
   extends: .build-template
   variables:
     OPAM_VARIANT: "+32bit"
     COQ_EXTRA_CONF: "-native-compiler yes"
-    COQIDE: "no"
+    ROCQIDE: "no"
   only: *full-ci
 
 build:edge+flambda:
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 83fdc41a1a0e8..059404fb6c8cb 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -232,7 +232,7 @@ manifesto's README][coq-community-manifesto].
 
 ### Contributing to the editor support packages ###
 
-Besides CoqIDE, whose sources are available in this repository, and to
+Besides Rocqide, whose sources are available in this repository, and to
 which you are welcome to contribute, there are a number of alternative
 user interfaces for Rocq, more often as an editor support package.
 
@@ -294,7 +294,7 @@ GitHub account).  You can file a bug for any of the following:
   find or don't understand some bit of documentation.
 - An error message that wasn't as helpful as you'd like. Bonus points
   for suggesting what information would have helped you.
-- Bugs in CoqIDE should also be filed in the [Rocq issue
+- Bugs in Rocqide should also be filed in the [Rocq issue
   tracker][Rocq-issue-tracker].  Bugs in the Emacs plugin should be
   filed against [ProofGeneral][ProofGeneral-issues], or against
   [company-coq][company-coq-issues] if they are specific to
diff --git a/INSTALL.md b/INSTALL.md
index be853454e714e..fb15658836769 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -34,7 +34,7 @@ To compile Rocq yourself, you need:
   ties to even as default rounding mode (most architectures
   should work nowadays)
 
-- for CoqIDE, the
+- for RocqIDE, the
   [lablgtk3-sourceview3](https://github.com/garrigue/lablgtk) library
   (version >= 3.1.2), and the corresponding GTK 3.x libraries, as
   of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18)
@@ -55,7 +55,7 @@ this moment) must be properly registered with `findlib/ocamlfind`
 since Rocq's build system uses `findlib` to locate them.
 
 Debian / Ubuntu users can get the necessary system packages for
-CoqIDE with:
+RocqIDE with:
 
     $ sudo apt-get install libgtksourceview-3.0-dev
 
@@ -87,14 +87,14 @@ but final users must always use the release build. See
 [dev/doc/build-system.dune.md](dev/doc/build-system.dune.md)
 for more details.
 
-To build and install Rocq (and CoqIDE if desired) do:
+To build and install Rocq (and RocqIDE if desired) do:
 
     $ ./configure -prefix <install_prefix> $options
     $ make dunestrap
-    $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,coqide
-    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coq coqide-server coqide
+    $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,rocqide
+    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coq coqide-server rocqide
 
-You can drop the `coqide` packages if not needed.
+You can drop the `rocqide` packages if not needed.
 
 Packagers may want to play with `dune install` options as to tweak
 installation path, the `-prefix` argument in `./configure` tells Rocq
diff --git a/Makefile b/Makefile
index 56102a4a94566..21372642224ee 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@
 
 # Dune Makefile for Coq
 
-.PHONY: help help-install states world coqide watch check    # Main developer targets
+.PHONY: help help-install states world rocqide watch check    # Main developer targets
 .PHONY: refman-html refman-pdf corelib-html apidoc     # Documentation targets
 .PHONY: test-suite dev-targets
 .PHONY: fmt ocheck obuild ireport clean               # Maintenance targets
@@ -39,9 +39,9 @@ help:
 	@echo "make help-install for installation instructions. Common developer targets are:"
 	@echo ""
 	@echo "  - states: build a minimal functional coqtop"
-	@echo "  - world:  build main public binaries and libraries in developer mode (no coqide)"
+	@echo "  - world:  build main public binaries and libraries in developer mode (no rocqide)"
 	@echo "  - watch:  build main public binaries and libraries [continuous build]"
-	@echo "  - coqide: build coqide binary in developer mode"
+	@echo "  - rocqide: build rocqide binary in developer mode"
 	@echo "  - check:  build all ML files as fast as possible"
 	@echo "  - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]"
 	@echo "  - dunestrap: Generate the dune rules for vo files"
@@ -51,7 +51,7 @@ help:
 	@echo "  Note: these targets produce a developer build, not suitable"
 	@echo "        for distribution to end-users or install"
 	@echo ""
-	@echo " To run an \$$app \\in {coqc,coqtop,coqtop.byte,coqide}:"
+	@echo " To run an \$$app \\in {coqc,coqtop,coqtop.byte,rocqide}:"
 	@echo ""
 	@echo "  - use 'dune exec -- dev/shim/\$$app args'"
 	@echo "    Example: 'dune exec -- dev/shim/coqc file.v'"
@@ -100,7 +100,7 @@ help-install:
 	@echo "  - coq-core: compat binaries (coqc instead of rocq compile, etc)"
 	@echo "  - rocq-core: Coq's prelude and corelib"
 	@echo "  - coqide-server: XML protocol language server"
-	@echo "  - coqide: CoqIDE gtk application"
+	@echo "  - rocqide: RocqIDE gtk application"
 	@echo "  - rocq: meta package depending on rocq-runtime rocq-core rocq-stdlib"
 	@echo "    (also calls the test suite when using --with-test)"
 	@echo "  - coq: meta package depending on rocq-runtime coq-core rocq-core rocq-stdlib coq-stdlib"
@@ -167,8 +167,8 @@ MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install coqide-ser
 world: dunestrap
 	dune build $(DUNEOPT) $(MAIN_TARGETS)
 
-coqide:
-	dune build $(DUNEOPT) coqide.install
+rocqide:
+	dune build $(DUNEOPT) rocqide.install
 
 watch:
 	dune build $(DUNEOPT) $(MAIN_TARGETS) -w
@@ -282,9 +282,9 @@ $(foreach subdir,$(wildcard theories/*/),$(eval $(call subtarget,$(subdir),$(she
 #
 # dune build rocq-runtime.install
 # dune build coq.install
-# dune build coqide.install
+# dune build rocqide.install
 #
 # Packaging / OPAM targets:
 #
 # dune -p coq @install
-# dune -p coqide @install
+# dune -p rocqide @install
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 83e1bd93e0df4..d97cdbc8b3b11 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -28,7 +28,7 @@ val ocamlfind : string
 (* used in envars for coq_makefile *)
 val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
 
-(* Used in coqide *)
+(* Used in rocqide *)
 val arch : string       (* architecture *)
 
 (* dubious use in envars, use in coqmakefile *)
@@ -45,7 +45,7 @@ val all_src_dirs : string list
 (* Used in micromega *)
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 
-(* Used in coqide *)
+(* Used in rocqide *)
 val browser : string
 (** default web browser to use, may be overridden by environment
     variable COQREMOTEBROWSER *)
@@ -57,7 +57,7 @@ val has_natdynlink : bool
 val wwwcoq : string
 val wwwstdlib : string
 
-(* used in coqide *)
+(* used in rocqide *)
 val wwwrefman : string
 
 (* for error reporting *)
diff --git a/coqide-server.opam b/coqide-server.opam
index e5c22ee147aee..fb50a26829e9b 100644
--- a/coqide-server.opam
+++ b/coqide-server.opam
@@ -10,7 +10,7 @@ semi-interactive development of machine-checked proofs.
 
 This package provides the `coqidetop` language server, an
 implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
-which allows clients, such as CoqIDE, to interact with Coq in a
+which allows clients, such as RocqIDE, to interact with Coq in a
 structured way."""
 maintainer: ["The Coq development team <coqdev@inria.fr>"]
 authors: ["The Coq development team, INRIA, CNRS, and contributors"]
diff --git a/default.nix b/default.nix
index c56282c026fce..b810bccf57c67 100644
--- a/default.nix
+++ b/default.nix
@@ -1,7 +1,7 @@
 # How to use?
 
 # If you have Nix installed, you can get in an environment with everything
-# needed to compile Coq and CoqIDE by running:
+# needed to compile Coq and RocqIDE by running:
 # $ nix-shell
 # at the root of the Coq repository.
 
@@ -111,7 +111,7 @@ stdenv.mkDerivation rec {
 
   enableParallelBuilding = true;
 
-  buildFlags = [ "world" ] ++ optional buildIde "coqide";
+  buildFlags = [ "world" ] ++ optional buildIde "rocqide";
 
   # TODO, building of documentation package when not in dev mode
   # https://github.com/coq/coq/issues/16198
@@ -120,7 +120,7 @@ stdenv.mkDerivation rec {
   # From https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/ocaml/dune.nix
   installPhase = ''
     runHook preInstall
-    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core coqide-server ${optionalString buildIde "coqide"}
+    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core coqide-server ${optionalString buildIde "rocqide"}
     runHook postInstall
   '';
 
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 2f59ccee60e68..0c6587a087137 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -8,7 +8,7 @@ unless these tests pass.
 We are currently running tests on the following platforms:
 
 - GitLab CI is the main CI platform. It tests the compilation of Coq,
-  of the documentation, and of CoqIDE on Linux with several versions
+  of the documentation, and of RocqIDE on Linux with several versions
   of OCaml and with warnings as errors; it runs the test-suite and
   tests the compilation of several external developments. It also runs
   a linter that checks whitespace discipline. A [pre-commit
diff --git a/dev/ci/platform/coq-pf-03-build.bat b/dev/ci/platform/coq-pf-03-build.bat
index 664f45abd7989..38b2450768e48 100644
--- a/dev/ci/platform/coq-pf-03-build.bat
+++ b/dev/ci/platform/coq-pf-03-build.bat
@@ -27,7 +27,7 @@ call coq_platform_make_windows.bat ^
   -override-dev-pkg="coq-core=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   -override-dev-pkg="coq=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   -override-dev-pkg="coqide-server=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
-  -override-dev-pkg="coqide=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
+  -override-dev-pkg="rocqide=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   || GOTO ErrorExit
 
 GOTO :EOF
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 752451414a128..845fe6ac2da5e 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -106,7 +106,7 @@ Dune will read the file `~/.config/dune/config`; see `man
 dune-config`. Among others, you can set in this file the custom number
 of build threads `(jobs N)` and display options `(display _mode_)`.
 
-## Running binaries [coqtop / coqide]
+## Running binaries [coqtop / rocqide]
 
 Running `coqtop` directly with `dune exec -- coqtop` won't in general
 work well unless you are using `dune exec -- coqtop -noinit`. The
@@ -114,13 +114,13 @@ work well unless you are using `dune exec -- coqtop -noinit`. The
 vo files may go stale if you rebuild only `coqtop`.
 
 Instead, you should use the provided "shims" for running `coqtop` and
-`coqide` in a fast build. In order to use them, do:
+`rocqide` in a fast build. In order to use them, do:
 
 ```
 $ dune exec -- dev/shim/coqtop
 ```
 
-or `quickide` / `dev/shim/coqide` for CoqIDE, etc.... See `dev/shim/dune` for a
+or `quickide` / `dev/shim/rocqide` for RocqIDE, etc.... See `dev/shim/dune` for a
 complete list of targets. These targets enjoy quick incremental compilation
 thanks to `-opaque` so they tend to be very fast while developing.
 
@@ -207,7 +207,7 @@ dune exec -- dev/dune-dbg coqc foo.v
 (ocd) source db
 ```
 
-to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`:
+to start `coqc.byte foo.v`, other targets are `{checker,rocqide,coqtop}`:
 
 ```
 dune exec -- dev/dune-dbg checker foo.vo
@@ -257,10 +257,10 @@ plugin will correctly track dependencies and rebuild incrementally as
 needed.
 
 However, it is not always desirable to go this way. For example, the
-current Coq source tree contains two packages [Coq and CoqIDE], and in
-the OPAM CoqIDE package we don't want to build CoqIDE against the
+current Rocq source tree contains two packages [Rocq and RocqIDE], and in
+the OPAM RocqIDE package we don't want to build RocqIDE against the
 local copy of Coq. For this purpose, Dune supports the `-p` option, so
-`dune build -p coqide` will build CoqIDE against the system-installed
+`dune build -p rocqide` will build RocqIDE against the system-installed
 version of Coq libs, and use a "release" profile that for example
 enables stronger compiler optimizations.
 
@@ -316,7 +316,7 @@ useful to Coq, some examples are:
 
   You are likely running a partial build which doesn't include
   implicitly loaded plugins / vo files. See the "Running binaries
-  [coqtop / coqide]" section above as to how to correctly call Coq's
+  [coqtop / rocqide]" section above as to how to correctly call Rocq's
   binaries.
 
 ## Dune cheat sheet
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 161eeffde28f5..5675c3da6a141 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -5,7 +5,7 @@ for his [vscoq](https://github.com/coq-community/vscoq/) project.
 
 Here, the aim is to provide a "hands on" description of the XML
 protocol that coqtop and IDEs use to communicate. The protocol first appeared 
-with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces.
+with Coq 8.5, and is used by RocqDE, [vscoq legacy](https://github.com/coq-community/vscoq-legacy/), and other user interfaces.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/v8.16/etc/notes/coq-notes.md).
@@ -331,7 +331,7 @@ many there are.
 -------------------------------
 
 ### <a name="command-status">**Status(force: bool)**</a>
-Returns information about the current proofs. CoqIDE typically sends this
+Returns information about the current proofs. RocqIDE typically sends this
 message with `force = false` after each sentence, and with `force = true` if
 the user wants to force the checking of all proofs (wheels button). In terms of
 the STM API, `force` triggers a `Join`.
@@ -544,7 +544,7 @@ Sends a list of option settings, where each setting roughly looks like:
   </list>
 </call>
 ```
-CoqIDE sends the following settings (defaults in parentheses):
+RocqIDE sends the following settings (defaults in parentheses):
 ```
 Printing Width : (<option_value val="intvalue"><int>60</int></option_value>),
 Printing Coercions : (<option_value val="boolvalue"><bool val="false"/></option_value>),
@@ -705,7 +705,7 @@ processed when Coq is no longer busy or execution stops in the debugger.
   <list>
     <pair>
       <pair>
-        <string>/home/proj/coq/ide/coqide/debug.v</string>
+        <string>/home/proj/coq/ide/rocqide/debug.v</string>
         <int>22</int>
       </pair>
       <bool val="true"/>
@@ -957,7 +957,7 @@ Currently these tags are used:
 * **goal** - the current goal for the debugger, for display in the Messages panel
   or elsewhere
 * **prompt** - output for display in the Messages panel prompting the user to
-  enter a debug command, allowing CoqIDE to display it without
+  enter a debug command, allowing RocqIDE to display it without
   appending a newline.  It also signals that coqidetop is waiting to receive
   a debugger-specific message such as [Db_cmd](#command-db_cmd).
 
@@ -984,8 +984,8 @@ There are 4 tags that indicate how the enclosed text should be highlighted:
 - diff.added.bg - unchanged text in a line that has additions ("bg" for "background")
 - diff.removed.bg - unchanged text in a line that has removals
 
-CoqIDE, Proof General and coqtop currently use 2 shades of green and 2 shades of red
-as the background color for highlights.  Coqtop and CoqIDE also apply underlining and/or
+RocqIDE, Proof General and coqtop currently use 2 shades of green and 2 shades of red
+as the background color for highlights.  Coqtop and RocqIDE also apply underlining and/or
 strikeout highlighting for the sake of the color blind.
 
 For example, `<diff.added>ABC</diff.added>` indicates that "ABC" should be highlighted
diff --git a/dev/dune b/dev/dune
index fb0f40a53a24a..b8dedfef5609a 100644
--- a/dev/dune
+++ b/dev/dune
@@ -24,7 +24,7 @@
     ../checker/coqchk.bc
     ../topbin/rocqworker.bc
     ../topbin/rocqnative.bc
-    ../ide/coqide/rocqide_main.bc
+    ../ide/rocqide/rocqide_main.bc
     ; We require all the OCaml libs to be in place and searchable
     ; by OCamlfind, this is a bit of a hack but until Dune gets
     ; proper ocamldebug support we have to live with that.
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 2ee4d072a8b6e..72d1da3e76ee5 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -19,9 +19,9 @@ while [[ $# -gt 0 ]]; do
             opts+=($(ocamlfind query -recursive -i-format rocq-runtime.checklib))
             break
             ;;
-        coqide)
+        rocqide)
             shift
-            exe=_build/default/ide/coqide/coqide_main.bc
+            exe=_build/default/ide/rocqide/rocqide_main.bc
             break
             ;;
         coqc)
@@ -40,7 +40,7 @@ while [[ $# -gt 0 ]]; do
             break
             ;;
         *)
-            echo "usage: dune exec -- dev/dune-dbg [-emacs] {coqchk|coqide|coqc|coqtop|coqdep|coqnative} coqargs"
+            echo "usage: dune exec -- dev/dune-dbg [-emacs] {coqchk|rocqide|coqc|coqtop|coqdep|coqnative} coqargs"
             exit 1
             ;;
     esac
diff --git a/dev/shim/dune b/dev/shim/dune
index 56bcdd216b190..726529064cde5 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -102,27 +102,27 @@
     (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
     (run chmod +x %{targets})))))
 
-; coqide
+; rocqide
 
 (alias
- (name coqide-prelude)
+ (name rocqide-prelude)
  (deps
   ; without this if the gtk libs are not available dune can try to use
-  ; coqide from PATH instead of giving a nice error
+  ; rocqide from PATH instead of giving a nice error
   ; there is no problem with the other shims since they don't depend on optional build products
-  %{project_root}/ide/coqide/rocqide_main.exe
+  %{project_root}/ide/rocqide/rocqide_main.exe
   %{bin:rocqworker}
   %{bin:coqidetop}
   %{project_root}/theories/Init/Prelude.vo
   %{project_root}/coqide-server.install
-  %{project_root}/coqide.install))
+  %{project_root}/rocqide.install))
 
 (rule
- (targets coqide)
- (deps (alias coqide-prelude))
+ (targets rocqide)
+ (deps (alias rocqide-prelude))
  (action
   (with-stdout-to %{targets}
    (progn
     (echo "#!/usr/bin/env bash\n")
-    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqide} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
+    (bash "echo '\"$(dirname \"$0\")\"/%{bin:rocqide} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
     (run chmod +x %{targets})))))
diff --git a/doc/changelog/10-coqide/00000-title.rst b/doc/changelog/10-coqide/00000-title.rst
deleted file mode 100644
index 81cf05b8440f0..0000000000000
--- a/doc/changelog/10-coqide/00000-title.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-
-CoqIDE
-^^^^^^
-
diff --git a/doc/changelog/10-rocqide/00000-title.rst b/doc/changelog/10-rocqide/00000-title.rst
new file mode 100644
index 0000000000000..e781c5c0e2e07
--- /dev/null
+++ b/doc/changelog/10-rocqide/00000-title.rst
@@ -0,0 +1,3 @@
+
+RocqIDE
+^^^^^^^
diff --git a/doc/changelog/10-coqide/19166-coqide.rst b/doc/changelog/10-rocqide/19166-coqide.rst
similarity index 100%
rename from doc/changelog/10-coqide/19166-coqide.rst
rename to doc/changelog/10-rocqide/19166-coqide.rst
diff --git a/doc/changelog/10-coqide/19188-warnings_in_table.rst b/doc/changelog/10-rocqide/19188-warnings_in_table.rst
similarity index 100%
rename from doc/changelog/10-coqide/19188-warnings_in_table.rst
rename to doc/changelog/10-rocqide/19188-warnings_in_table.rst
diff --git a/doc/changelog/10-coqide/19417-coqide-preferences.rst b/doc/changelog/10-rocqide/19417-coqide-preferences.rst
similarity index 100%
rename from doc/changelog/10-coqide/19417-coqide-preferences.rst
rename to doc/changelog/10-rocqide/19417-coqide-preferences.rst
diff --git a/doc/changelog/10-rocqide/20036-rename-coqide.rst b/doc/changelog/10-rocqide/20036-rename-coqide.rst
new file mode 100644
index 0000000000000..885c4819546a3
--- /dev/null
+++ b/doc/changelog/10-rocqide/20036-rename-coqide.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  CoqIDE is renamed to RocqIDE (the auxiliary binary `coqidetop` is not renamed)
+  (`#20036 <https://github.com/coq/coq/pull/20036>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst b/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst
index d23e128dffde6..cb9d01cacfc4b 100644
--- a/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst
+++ b/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst
@@ -1,5 +1,5 @@
 - **Changed:**
-  when building Coq, the makefile's `world` target and `dune build`'s default target do not build coqide anymore.
-  Use `make world coqide` or `dune build @default coqide.install` to build what they respectively used to build
+  when building Coq, the makefile's `world` target and `dune build`'s default target do not build rocqide anymore.
+  Use `make world rocqide` or `dune build @default rocqide.install` to build what they respectively used to build
   (`#19378 <https://github.com/coq/coq/pull/19378>`_,
   by Gaëtan Gilbert).
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index e790d20e00c50..4b296a029d4b6 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -93,7 +93,7 @@
 \newcommand{\Coq}{\textsc{Coq}}
 \newcommand{\gallina}{\textsc{Gallina}}
 \newcommand{\Gallina}{\textsc{Gallina}}
-\newcommand{\CoqIDE}{\textsc{CoqIDE}}
+\newcommand{\RocqIDE}{\textsc{RocqIDE}}
 \newcommand{\ocaml}{\textsc{OCaml}}
 \newcommand{\camlpppp}{\textsc{Camlp5}}
 \newcommand{\emacs}{\textsc{GNU Emacs}}
diff --git a/doc/sphinx/_static/diffs-coqide-compacted.png b/doc/sphinx/_static/diffs-rocqide-compacted.png
similarity index 100%
rename from doc/sphinx/_static/diffs-coqide-compacted.png
rename to doc/sphinx/_static/diffs-rocqide-compacted.png
diff --git a/doc/sphinx/_static/diffs-coqide-multigoal.png b/doc/sphinx/_static/diffs-rocqide-multigoal.png
similarity index 100%
rename from doc/sphinx/_static/diffs-coqide-multigoal.png
rename to doc/sphinx/_static/diffs-rocqide-multigoal.png
diff --git a/doc/sphinx/_static/diffs-coqide-on.png b/doc/sphinx/_static/diffs-rocqide-on.png
similarity index 100%
rename from doc/sphinx/_static/diffs-coqide-on.png
rename to doc/sphinx/_static/diffs-rocqide-on.png
diff --git a/doc/sphinx/_static/diffs-coqide-removed.png b/doc/sphinx/_static/diffs-rocqide-removed.png
similarity index 100%
rename from doc/sphinx/_static/diffs-coqide-removed.png
rename to doc/sphinx/_static/diffs-rocqide-removed.png
diff --git a/doc/sphinx/_static/coqide-preferences-editor.png b/doc/sphinx/_static/rocqide-preferences-editor.png
similarity index 100%
rename from doc/sphinx/_static/coqide-preferences-editor.png
rename to doc/sphinx/_static/rocqide-preferences-editor.png
diff --git a/doc/sphinx/_static/coqide-preferences-shortcuts.png b/doc/sphinx/_static/rocqide-preferences-shortcuts.png
similarity index 100%
rename from doc/sphinx/_static/coqide-preferences-shortcuts.png
rename to doc/sphinx/_static/rocqide-preferences-shortcuts.png
diff --git a/doc/sphinx/_static/coqide-queries.png b/doc/sphinx/_static/rocqide-queries.png
similarity index 100%
rename from doc/sphinx/_static/coqide-queries.png
rename to doc/sphinx/_static/rocqide-queries.png
diff --git a/doc/sphinx/_static/coqide.png b/doc/sphinx/_static/rocqide.png
similarity index 100%
rename from doc/sphinx/_static/coqide.png
rename to doc/sphinx/_static/rocqide.png
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 89bcbb2232bc3..85b76cfc67dca 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -7,7 +7,7 @@ Asynchronous and Parallel Proof Processing
 
 This chapter explains how proofs can be asynchronously processed by
 Rocq. This feature improves the reactivity of the system when used in
-interactive mode via CoqIDE. In addition, it allows Rocq to take
+interactive mode via RocqIDE. In addition, it allows Rocq to take
 advantage of parallel hardware when used as a batch compiler by
 decoupling the checking of statements and definitions from the
 construction and checking of proofs objects.
@@ -26,7 +26,7 @@ category are universe inconsistencies.
 At the time of writing, only opaque proofs (ending with :cmd:`Qed` or
 :cmd:`Admitted`) can be processed asynchronously.
 
-Finally, asynchronous processing is disabled when running CoqIDE in
+Finally, asynchronous processing is disabled when running RocqIDE in
 Windows. The current implementation of the feature is not stable on
 Windows. It can be enabled, as described below at :ref:`interactive-mode`,
 though doing so is not recommended.
@@ -121,13 +121,13 @@ Caveats
 When a command fails the subsequent error messages may be
 bogus, i.e. caused by the first error. Error resilience for
 commands can be switched off by passing ``-async-proofs-command-error-resilience off``
-to CoqIDE.
+to RocqIDE.
 
 An incorrect proof block detection can result into an incorrect error
 recovery and hence in bogus errors. Proof block detection cannot be
 precise for bullets or any other non-well parenthesized proof
 structure. Error resilience can be turned off or selectively activated
-for any set of block kind passing to CoqIDE one of the following
+for any set of block kind passing to RocqIDE one of the following
 options:
 
 - ``-async-proofs-tactic-error-resilience off``
@@ -143,13 +143,13 @@ Interactive mode
 
 .. todo: How about PG and coqtail?
 
-CoqIDE and VsCoq support asynchronous proof processing.
+RocqIDE and VsCoq support asynchronous proof processing.
 
-When CoqIDE is started and async mode is enabled, two or more Rocq processes
+When RocqIDE is started and async mode is enabled, two or more Rocq processes
 are created. The master one
 follows the user, giving feedback as soon as possible by skipping
 proofs, which are delegated to the worker processes. The worker processes
-asynchronously processes the proofs.  The *Jobs panel* in the main CoqIDE
+asynchronously processes the proofs.  The *Jobs panel* in the main RocqIDE
 window shows the status of each worker process.
 If a proof contains an error, it's reported in red in the label of
 the very same button, that can also be used to see the list of errors
@@ -180,20 +180,20 @@ all the shells from which Rocq processes will be started.  If one uses just
 one terminal running the bash shell, then `export $(rocq workmgr -j 4)` will
 do the job.
 
-After that, all Coq processes, e.g. `coqide` and `rocq compile`,
+After that, all Coq processes, e.g. `rocqide` and `rocq compile`,
 will honor the limit, globally.
 
 Caveats
 ```````
 
-The number of worker processes can be increased by passing CoqIDE
+The number of worker processes can be increased by passing RocqIDE
 the ``-async-proofs-j n`` flag. Note that the memory consumption increases too,
 since each worker requires the same amount of memory as the master
 process. Also note that increasing the number of workers may reduce
 the reactivity of the master process to user commands.
 
 To disable this feature, one can pass the ``-async-proofs off`` flag to
-CoqIDE. Conversely, on Windows, where the feature is disabled by
+RocqIDE. Conversely, on Windows, where the feature is disabled by
 default, pass the ``-async-proofs on`` flag to enable it.
 
 Proofs that are known to take little time to process are not delegated
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index a88bc515c91aa..61ad165da49db 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -4577,7 +4577,7 @@ CoqIDE
   visually and jumping to the stopping point plus continue, step over,
   step in and step out operations.  Displays the call stack and
   variable values for each stack frame.  Currently only for Ltac.
-  See the documentation :ref:`here <coqide-debugger>`
+  See the documentation :ref:`here <rocqide-debugger>`
   (`#14644 <https://github.com/coq/coq/pull/14644>`_,
   fixes `#13967 <https://github.com/coq/coq/issues/13967>`_,
   by Jim Fehrle)
@@ -8689,7 +8689,7 @@ reference manual. Here are the most important user-visible changes:
     ``\alpha`` then ``Shift+Space`` will insert the greek letter alpha.
     A larger number of default bindings are provided, following the latex
     naming convention. Bindings can be customized, either globally, or on a
-    per-project basis. See Section :ref:`coqide-unicode` for details
+    per-project basis. See Section :ref:`rocqide-unicode` for details
     (`#8560 <https://github.com/coq/coq/pull/8560>`_, by Arthur Charguéraud).
 
 - Infrastructure and dependencies:
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 41368d74efb83..d49c550d90f09 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/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 `rocq repl`, definitions in the script are associated
+buffer in RocqIDE 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
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 794c9f6513342..2c3d0c2009b95 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -5,7 +5,7 @@ The Rocq Prover commands
 
 There are several Rocq commands:
 
-+ ``coqide``: a graphical integrated development environment, described
++ ``rocqide``: a graphical integrated development environment, described
   :ref:`here <coqintegrateddevelopmentenvironment>`.  In addition, there are
   several other IDEs such as Proof General, vsCoq and Coqtail that are not
   included with the Coq installation.
@@ -61,13 +61,13 @@ See :ref:`rocq_makefile` and :ref:`building_dune`.
    To compile `foo.v` as part of a module `Mod1` that is rooted
    at `.` (i.e. the directory containing `foo.v`), run `rocq c -Q . Mod1 foo.v`.
 
-   To make the module available in `CoqIDE`, include the following line in the
+   To make the module available in `RocqIDE`, include the following line in the
    `_CoqProject` file (see :ref:`rocq_makefile`) in the directory from which you
-   start `CoqIDE` or give it as an argument to the ``coqide`` command.
+   start `RocqIDE` or give it as an argument to the ``rocqide`` command.
    *<PATH>* is the pathname of the directory containing the module,
    which can be an absolute path or relative to Rocq's current directory.  For now,
-   you must close and reload a named script file for `CoqIDE` to pick up the change,
-   or restart `CoqIDE`.
+   you must close and reload a named script file for `RocqIDE` to pick up the change,
+   or restart `RocqIDE`.
    The project file name is configurable in `Edit / Preferences / Project`.
 
       .. rocqdoc::
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index ca11dd21b2244..73a3e68104766 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -2,29 +2,29 @@
 
 .. _coqintegrateddevelopmentenvironment:
 
-CoqIDE
-======
+RocqIDE
+=======
 
 .. todo: how to say that a number of things are broken?  Maybe list them
    somewhere--doesn't have to be super detailed
 
-The Coq Integrated Development Environment (CoqIDE) is a user-friendly GUI
+The Rocq Integrated Development Environment (RocqIDE) is a user-friendly GUI
 for Coq. Its main purpose is to allow users to edit Coq scripts and step forward
 and backward through them.  Stepping forward executes commands and
 tactics while stepping backward undoes previously executed commands and tactics,
 returning to a previous state.
 
-To run CoqIDE, enter `coqide` on the command line.
+To run RocqIDE, enter `rocqide` on the command line.
 If you include script file names (which end with `.v`) as arguments, each is opened
-in a separate tab.  If you don't, CoqIDE opens a single unnamed buffer
-(titled `*scratch*`).  `coqide` also accepts many of the options of `coqtop`
+in a separate tab.  If you don't, RocqIDE opens a single unnamed buffer
+(titled `*scratch*`).  `rocqide` also accepts many of the options of `rocq top`
 (see :ref:`therocqcommands`), while ignoring the ones that aren't meaningful
-for CoqIDE.  Use `coqide --help` to see the list of command line options.
+for RocqIDE.  Use `rocqide --help` to see the list of command line options.
 
-.. _coqide_mainscreen:
+.. _rocqide_mainscreen:
 
-.. image:: ../_static/coqide.png
-   :alt: CoqIDE main screen
+.. image:: ../_static/rocqide.png
+   :alt: RocqIDE main screen
 
 ..  Here is the code used in the screenshot:
 
@@ -41,7 +41,7 @@ for CoqIDE.  Use `coqide --help` to see the list of command line options.
     Proof.
       Induction n.
 
-The screenshot shows CoqIDE as the user is stepping through the file `Fermat.v`.
+The screenshot shows RocqIDE as the user is stepping through the file `Fermat.v`.
 
 A menu bar and a tool bar appear at the top of the window. The left-hand panel shows
 the current *script buffer*.  Each script buffer corresponds to a separate Coq process.
@@ -90,10 +90,10 @@ the cursor between `(*` and `*)` or select any text between them.
 
 Files are automatically saved periodically to a recovery file.  For example,
 `foo.v` is saved to `#foo.v#` every 10 seconds by default.  You can change the
-interval in the *Edit / Preferences / Files* dialog.  In some cases when CoqIDE
-exits abruptly, it saves named buffers in ``<NAME>.crashcoqide`` in the same
+interval in the *Edit / Preferences / Files* dialog.  In some cases when RocqIDE
+exits abruptly, it saves named buffers in ``<NAME>.crashrocqide`` in the same
 directory as ``<NAME>``.  Unnamed buffers are saved in
-``Unnamed_coqscript_<N>.crashcoqide`` in the directory that CoqIDE was started in.
+``Unnamed_rocqscript_<N>.crashrocqide`` in the directory that RocqIDE was started in.
 
 In the *View* menu, you can set several printing options that
 correspond to options that can appear in the script.  For example, *Display
@@ -112,8 +112,8 @@ from the toolbar and from the keyboard.  These include:
 - Reset Coq (`Alt-Home`) to restart the Coq process
 - Run to end (`Alt-End`) to run commands to the end of the buffer
 - Interrupt to stop processing commands after the current command completes.
-  (Note: on Windows but not on WSL, Interrupt doesn't work if you start CoqIDE
-  as a background process, e.g. `coqide &` in bash.  See Coq issue
+  (Note: on Windows but not on WSL, Interrupt doesn't work if you start RocqIDE
+  as a background process, e.g. `rocqide &` in bash.  See Rocq issue
   `#16142 <https://github.com/coq/coq/pull/16142>`_.)
 
 On macOS, use `Cmd-Ctrl` instead of `Alt` for these operations.
@@ -137,7 +137,7 @@ Commands may:
   Double click on an entry to jump to the point of the error.  Execution
   of commands stops unless you're in async mode.
 
-In the previous figure :ref:`CoqIDE main screen <coqide_mainscreen>`,
+In the previous figure :ref:`RocqIDE main screen <rocqide_mainscreen>`,
 the running buffer is `Fermat.v`.  All commands until
 the ``Theorem`` have already been executed, then the user tried to go
 forward executing ``Induction n``. That command failed because no such
@@ -159,7 +159,7 @@ The other buttons on the toolbar do the following:
 - Next occurrence (right arrow icon) - find the next occurrence
   of the current word
 
-The colored ribbon appearing across the bottom of the CoqIDE window just above
+The colored ribbon appearing across the bottom of the RocqIDE window just above
 the status bar represents the state of processing for the current script
 schematically.  Blue means unprocessed, light green means successfully
 processed, red mean an error, light orange is used for :cmd:`Axiom` and :cmd:`Admitted`
@@ -169,7 +169,7 @@ in the async mode section.)
 
 The left edge of the ribbon corresponds to the first command or tactic in the
 script and the right edge corresponds to the last command that has been passed
-to Coq.  Currently, for very long scripts, it may take many seconds for CoqIDE to
+to Rocq.  Currently, for very long scripts, it may take many seconds for RocqIDE to
 pass all the commands to the server, causing the display to jump around a lot.  Perhaps
 this will be improved in a future release.  The text at the far right hand side of
 the status bar (e.g. "0 / 1" gives the number of unprocessed proofs that have been
@@ -218,8 +218,8 @@ commands like ``Fixpoint`` that you can conveniently fill in afterwards.
 Queries
 -------
 
-.. image:: ../_static/coqide-queries.png
-   :alt: CoqIDE queries
+.. image:: ../_static/rocqide-queries.png
+   :alt: RocqIDE queries
 
 A *query* is any command that does not change the current state, such as
 :cmd:`About`, :cmd:`Check`, :cmd:`Print`, :cmd:`Search`, etc.  The *query pane*
@@ -257,7 +257,7 @@ the *Externals* section of the *Edit/Preferences* dialog.  Output appears in the
 in :ref:`here <building_with_coqproject>`.  Alternatively, you may find it easier
 to do your `make` and `rocq makefile` commands from the command line.
 
-.. _coqide_make_note:
+.. _rocqide_make_note:
 
 Note that you must explicitly save changed buffers before you run `make`.
 *File/Save all* is helpful for this.  Notice that modified and unmodified buffers show
@@ -284,14 +284,14 @@ Preferences
 You may customize your environment with the *Preferences* dialog, which is
 accessible from *Edit/Preferences* on the menu. There are several sections.
 
-.. image:: ../_static/coqide-preferences-editor.png
-   :alt: CoqIDE preferences dialog, Editor section
+.. image:: ../_static/rocqide-preferences-editor.png
+   :alt: RocqIDE preferences dialog, Editor section
 
 The *Files* section is devoted to file management: you may configure
 automatic saving of files, by periodically saving the contents into
 files named `#f#` for each opened file `f`. You may also activate the
 *auto reload* feature: in case an opened file is modified on disk by a
-third party, CoqIDE may read it again for you. Note that in the case
+third party, RocqIDE may read it again for you. Note that in the case
 you edited that same file, you will be prompted to choose to either
 discard your changes or not. The File charset encoding choice is
 described below in :ref:`character-encoding-saved-files`.
@@ -304,7 +304,7 @@ customizing the editor. It includes in particular the ability
 to activate an Emacs mode named micro-Proof-General
 (use the Help menu to know more about the available bindings).
 
-The *Appearance* section offers controls to set CoqIDE's window
+The *Appearance* section offers controls to set RocqIDE's window
 default size and the position of tabs.
 
 The *Fonts* section is for selecting the text font used for scripts,
@@ -316,7 +316,7 @@ as standard |GtkSourceView| styles are available. Other styles can be
 added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see
 the general documentation about |GtkSourceView| for the various
 possibilities). Note that the style of the rest of graphical part of
-CoqIDE is not under the control of |GtkSourceView| but of GTK+ and
+RocqIDE is not under the control of |GtkSourceView| but of GTK+ and
 governed by files such as ``settings.ini`` and ``gtk.css`` in
 ``$XDG_CONFIG_HOME/gtk-3.0`` or files in
 ``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment
@@ -352,7 +352,7 @@ is set.  If the variable isn't set, the directory is ``~/.config/coq`` on Linux
 and `C:\\Users\\<USERNAME>\\AppData\\Local\\coq` on Windows.
 Preferences are in the file `coqiderc` and key bindings are in the file `coqide.keys`.
 
-.. _coqide_key_bindings:
+.. _rocqide_key_bindings:
 
 .. _key_bindings:
 
@@ -363,8 +363,8 @@ As explained just above, the *Edit/Preferences/Shortcuts* panel
 offers buttons to modify in a few clicks the key bindings for a whole menu.
 Here is a screenshot of the panel:
 
-.. image:: ../_static/coqide-preferences-shortcuts.png
-   :alt: CoqIDE preferences dialog, Shortcuts section
+.. image:: ../_static/rocqide-preferences-shortcuts.png
+   :alt: RocqIDE preferences dialog, Shortcuts section
 
 Each menu item in the GUI shows its key binding, if one has been defined,
 on the right-hand side.  Typing the key binding is equivalent to selecting
@@ -376,8 +376,8 @@ for the new binding and then releasing the mouse button.
 Alternatively, you can edit the configuration file directly.
 Key bindings are saved in the file `coqide.keys` in
 the :ref:`user configuration directory<user-configuration-directory>`.
-Make sure there are no CoqIDE processes running while you edit the file
-(CoqIDE creates or overwrites the file when it terminates,
+Make sure there are no RocqIDE processes running while you edit the file
+(RocqIDE creates or overwrites the file when it terminates,
 which may reorder the lines).
 
 The file contains lines such as:
@@ -393,14 +393,14 @@ which was bound by default to `Shift-Ctrl-A`. `<Primary>` indicates `Cmd` on mac
 and otherwise `Ctrl`.
 The second line is for a menu item that has no key binding.
 
-Lines that begin with semicolons are comments created by CoqIDE.  CoqIDE uses
+Lines that begin with semicolons are comments created by RocqIDE.  RocqIDE uses
 the default binding for these items.  To change a key binding, remove the semicolon
 and set the third item in the list as desired, such as in the third line.
 Avoid assigning the same binding to multiple items.
 
 If the same menu item name appears on multiple lines in the file, the value from the
 last line is used.  This is convenient for copying a group of changes from elsewhere–just
-insert the changes at the end of the file.  The next time CoqIDE terminates, it will
+insert the changes at the end of the file.  The next time RocqIDE terminates, it will
 resort the items.
 
 The end of
@@ -417,9 +417,9 @@ Edit/Preferences/Shortcuts panel. See :ref:`Shortcuts<shortcuts>`.
 Using Unicode symbols
 ---------------------
 
-CoqIDE is based on GTK+ and inherits from it support for Unicode in
+RocqIDE is based on GTK+ and inherits from it support for Unicode in
 its text panels. Consequently a large set of symbols is available for
-notations. Furthermore, CoqIDE conveniently provides a simple way to
+notations. Furthermore, RocqIDE conveniently provides a simple way to
 input Unicode characters.
 
 
@@ -440,8 +440,8 @@ mathematical symbols ∀ and ∃, you may define:
      : type_scope.
 
 A small set of such notations are already defined in the Coq library
-which you can enable with ``Require Import Unicode.Utf8`` inside CoqIDE,
-or equivalently, by starting CoqIDE with ``coqide -l utf8``.
+which you can enable with ``Require Import Unicode.Utf8`` inside RocqIDE,
+or equivalently, by starting RocqIDE with ``rocqide -l utf8``.
 
 However, there are some issues when using such Unicode symbols: you of
 course need to use a character font which supports them. In the Fonts
@@ -452,12 +452,12 @@ use antialiased fonts or not, by setting the environment variable
 `GDK_USE_XFT` to 1 or 0 respectively.
 
 
-.. _coqide-unicode:
+.. _rocqide-unicode:
 
 Bindings for input of Unicode symbols
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-CoqIDE supports a builtin mechanism to input non-ASCII symbols.
+RocqIDE supports a builtin mechanism to input non-ASCII symbols.
 For example, to input ``π``, it suffices to type ``\pi`` then press the
 combination of key ``Ctrl-Space`` (default key binding). Often, it
 suffices to type a prefix of the LaTeX token, e.g. typing ``\p``
@@ -468,7 +468,7 @@ right arrow, or ``\>=`` for a greater than or equal sign.
 
 A larger number of LaTeX tokens are supported by default. The full list
 is available here:
-https://github.com/coq/coq/blob/master/ide/coqide/default_bindings_src.ml
+https://github.com/coq/coq/blob/master/ide/rocqide/default_bindings_src.ml
 
 Custom bindings may be added, as explained further on.
 
@@ -478,7 +478,7 @@ of the preferences.
 .. note::
 
     It remains possible to input non-ASCII symbols using system-wide
-    approaches independent of CoqIDE.
+    approaches independent of RocqIDE.
 
 
 Adding custom bindings
@@ -508,7 +508,7 @@ Similarly, the above settings ensure than ``\l`` resolves to ``\le``,
 and that ``\la`` resolves to ``\lambda``.
 
 It can be useful to work with per-project binding files. For this purpose
-CoqIDE accepts a command line argument of the form
+RocqIDE accepts a command line argument of the form
 ``-unicode-bindings file1,file2,...,fileN``.
 Each of the file tokens provided may consists of one of:
 
@@ -542,7 +542,7 @@ related to the way files are saved.
 If you have no need to exchange files with non-UTF-8 aware
 applications, it is better to choose the UTF-8 encoding, since it
 guarantees that your files will be read again without problems. (This
-is because when CoqIDE reads a file, it tries to automatically detect
+is because when RocqIDE reads a file, it tries to automatically detect
 its character encoding.)
 
 If you choose something else than UTF-8, then missing characters will
@@ -550,13 +550,13 @@ be written encoded by `\x{....}` or `\x{........}` where each dot is
 an hexadecimal digit: the number between braces is the hexadecimal
 Unicode index for the missing character.
 
-.. _coqide-debugger:
+.. _rocqide-debugger:
 
 Debugger
 --------
 
 Version 8.15 introduces a visual debugger for |Ltac| tactics within
-CoqIDE.  It supports setting breakpoints visually and automatically
+RocqIDE.  It supports setting breakpoints visually and automatically
 displaying the stopping point in the source code with "continue",
 "step over" "step in" and "step out" operations.  The call stack and variable
 values for each stack frame are shown in a new panel.
@@ -581,7 +581,7 @@ shown with a dark blue background.  `Set Ltac Debug.` enables stopping in the
 debugger.
 
 .. image:: ../_static/debugger.png
-   :alt: CoqIDE Debugger
+   :alt: RocqIDE Debugger
 
 .. created with:
    Set Ltac Debug.  (* enable the debugger *)
@@ -647,7 +647,7 @@ Break (F11)
   Stops the debugger at the next possible stopping point, from which you can
   step or continue.   (Not supported in Windows at this time.)
 
-Note that the debugger is disabled when CoqIDE is running multiple worker processes,
+Note that the debugger is disabled when RocqIDE is running multiple worker processes,
 i.e. running in async mode.  Going "Forward" a single step at a time doesn't use
 async mode and will always enter the debugger as expected.  In addition, the debugger
 doesn't work correctly in some cases involving editing failed proofs in asymc mode (
@@ -671,7 +671,7 @@ indication that this has happened.
 
 .. unfortunately not working:
    Note: This `Wiki page <https://github.com/coq/coq/wiki/Configuration-of-CoqIDE#the-alternative-set-of-bindings>`_
-   describes a way to change CoqIDE key bindings.
+   describes a way to change RocqIDE key bindings.
 
 Call Stack and Variables
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -740,7 +740,7 @@ If a debugger instance is stopped in a secondary script, the debugger function
 keys are directed to the debugger instance associated with the primary script.
 The debugger doesn't attempt to support multiple instances
 stopped in the same secondary script.  If you have a need to do this, run
-each debugger instance in a separate CoqIDE process/window.
+each debugger instance in a separate RocqIDE process/window.
 
 Note that if you set a breakpoint in a script that may be called by multiple debugger
 instances, you may inadvertently find you've gotten into unsupported territory.
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 342f9a84cc964..98a94b6b36d39 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -196,9 +196,9 @@ We recommend checking `CoqMakefile` and `CoqMakefile.conf` into your source code
 control system.  Also we recommend updating them with `rocq makefile` when you switch
 to a new version of Rocq.
 
-In CoqIDE, you must explicitly save modified buffers before running `make` and
+In RocqIDE, you must explicitly save modified buffers before running `make` and
 restart the Rocq interpreter in any buffers in which you're running code.
-More details :ref:`here <coqide_make_note>`.
+More details :ref:`here <rocqide_make_note>`.
 
 See :ref:`rocq_makefile` for a complete description of `rocq makefile` and the
 files it generates.
@@ -244,7 +244,7 @@ permits loading files from the
 associated directory with just the basename of the script file,
 e.g. specify `Foo` to load `Foo.vo`.  This entry corresponds to the
 current directory when Rocq was started.  Note that the :cmd:`Cd` command
-doesn't change the associated directory--you would need to restart CoqIDE.
+doesn't change the associated directory--you would need to restart RocqIDE.
 
 With some exceptions noted below, the :term:`load path` is generated from files loaded
 from the following directories and their subdirectories in the order shown.  The
@@ -262,7 +262,7 @@ directory, e.g. the file `Foo/Bar/script.vo` becomes `Foo.Bar.script`:
 
 - the ``${XDG_DATA_HOME}/coq/`` directory (see `XDG base directory specification
   <http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_).
-  However, CoqIDE relies on the default setting; therefore we recommend not
+  However, RocqIDE relies on the default setting; therefore we recommend not
   setting this variable.
 - installed packages from the `user-contrib` directory in the Rocq installation,
 - the Rocq standard library from the `theories` directory in the Rocq installation
@@ -438,7 +438,7 @@ name, e.g. ``DECLARE PLUGIN "my-package.plugin"``.
 The ``-native-compiler`` option given in the ``_CoqProject`` file overrides
 the global one passed at configure time.
 
-CoqIDE, Proof General, VsCoq and Coqtail all
+RocqIDE, Proof General, VsCoq and Coqtail all
 understand ``_CoqProject`` files and can be used to invoke Rocq with the desired options.
 
 The ``rocq makefile`` utility can be used to set up a build infrastructure
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0fd6387de6931..847e94c1a853f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -2400,8 +2400,8 @@ Interactive debugger
 
    This flag, when set, enables the step-by-step debugger in the |Ltac| interpreter.
    The debugger is supported in `rocq repl` and Proof General by printing information
-   on the console and accepting typed commands.  In addition, CoqIDE now supports a
-   :ref:`visual debugger <coqide-debugger>` with additional capabilities.
+   on the console and accepting typed commands.  In addition, RocqIDE now supports a
+   :ref:`visual debugger <rocqide-debugger>` with additional capabilities.
 
 When the debugger is activated in `rocq repl`, it stops at every step of the evaluation of
 the current |Ltac| expression and prints information on what it is doing.
@@ -2431,7 +2431,7 @@ A non-interactive mode for the debugger is available via the flag:
 
    This flag has the effect of presenting a newline at every prompt, when
    the debugger is on in `rocq repl`.  (It has no effect when running the
-   CoqIDE debugger.)  The debug log thus created, which does not require
+   RocqIDE debugger.)  The debug log thus created, which does not require
    user input to generate when this flag is set, can then be run through
    external tools such as diff.
 
diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index 84b365f9d9d47..b7bd321944f68 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -11,7 +11,7 @@ you complete a proof, such as with the :cmd:`Qed` command.  Tactics,
 which are available only in proof mode, incrementally transform incomplete
 proofs to eventually generate a complete proof.
 
-When you run Rocq interactively, such as through CoqIDE, Proof General or
+When you run Rocq interactively, such as through RocqIDE, Proof General or
 `rocq repl`, Rocq shows the current proof state (the incomplete proof) as you
 enter tactics.  This information isn't shown when you run Rocq in batch
 mode with `rocq compile`.
@@ -1034,7 +1034,7 @@ Showing differences between proof steps
 Rocq can automatically highlight the differences between successive proof steps
 and between values in some error messages.  Rocq can also highlight differences
 in the proof term.
-For example, the following screenshots of CoqIDE and coqtop show the application
+For example, the following screenshots of RocqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
 to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
@@ -1057,25 +1057,25 @@ new, no line of old text is shown for them.
 
 ..
 
-  .. image:: ../../_static/diffs-coqide-on.png
-     :alt: CoqIDE with Set Diffs on
+  .. image:: ../../_static/diffs-rocqide-on.png
+     :alt: RocqIDE with Set Diffs on
 
 ..
 
-  .. image:: ../../_static/diffs-coqide-removed.png
-     :alt: CoqIDE with Set Diffs removed
+  .. image:: ../../_static/diffs-rocqide-removed.png
+     :alt: RocqIDE with Set Diffs removed
 
 ..
 
   .. image:: ../../_static/diffs-coqtop-on3.png
      :alt: coqtop with Set Diffs on
 
-This image shows an error message with diff highlighting in CoqIDE:
+This image shows an error message with diff highlighting in RocqIDE:
 
 ..
 
   .. image:: ../../_static/diffs-error-message.png
-     :alt: CoqIDE error message with diffs
+     :alt: RocqIDE error message with diffs
 
 How to enable diffs
 ```````````````````
@@ -1098,8 +1098,8 @@ Colors for `rocq repl` can be configured by setting the ``ROCQ_COLORS`` environm
 variable.  See section :ref:`customization-by-environment-variables`.  Diffs
 use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.
 
-In CoqIDE, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
-command in CoqIDE.  You can change the background colors shown for diffs from the
+In RocqIDE, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
+command in RocqIDE.  You can change the background colors shown for diffs from the
 ``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
 ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
 lets you control other attributes of the highlights, such as the foreground
@@ -1177,16 +1177,16 @@ the split because it has not changed.
 
 ..
 
-  .. image:: ../../_static/diffs-coqide-multigoal.png
-     :alt: coqide with Set Diffs on with multiple goals
+  .. image:: ../../_static/diffs-rocqide-multigoal.png
+     :alt: rocqide with Set Diffs on with multiple goals
 
 Diffs may appear like this after applying a :tacn:`intro` tactic that results
 in a compacted hypotheses:
 
 ..
 
-  .. image:: ../../_static/diffs-coqide-compacted.png
-     :alt: coqide with Set Diffs on with compacted hypotheses
+  .. image:: ../../_static/diffs-rocqide-compacted.png
+     :alt: rocqide with Set Diffs on with compacted hypotheses
 
 .. _showing_proof_diffs:
 
@@ -1197,7 +1197,7 @@ To show differences in the proof term:
 
 - In `rocq repl` and Proof General, use the :cmd:`Show Proof` `Diffs` command.
 
-- In CoqIDE, position the cursor on or just after a tactic to compare the proof term
+- In RocqIDE, position the cursor on or just after a tactic to compare the proof term
   after the tactic with the proof term before the tactic, then select
   `View / Show Proof` from the menu or enter the associated key binding.
   Differences will be shown applying the current `Show Diffs` setting
@@ -1209,7 +1209,7 @@ To show differences in the proof term:
   ..
 
     .. image:: ../../_static/diffs-show-proof.png
-       :alt: coqide with Set Diffs on with compacted hypotheses
+       :alt: rocqide with Set Diffs on with compacted hypotheses
 
 Delaying solving unification constraints
 ----------------------------------------
diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst
index 781411b7e67c9..5fb433b15eb42 100644
--- a/doc/sphinx/using/tools/index.rst
+++ b/doc/sphinx/using/tools/index.rst
@@ -5,9 +5,9 @@ Command-line and graphical tools
 ================================
 
 This chapter presents the command-line tools that users will need to
-build their Rocq project, the documentation of the CoqIDE graphical
+build their Rocq project, the documentation of the RocqIDE graphical
 user interface and the documentation of the parallel proof processing
-feature that is supported by CoqIDE and several other GUIs.
+feature that is supported by RocqIDE and several other GUIs.
 A list of available user interfaces to interact with Rocq is available
 on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_.
 
diff --git a/dune-project b/dune-project
index 63c9eca26f38d..657f209e2deaa 100644
--- a/dune-project
+++ b/dune-project
@@ -88,11 +88,11 @@ semi-interactive development of machine-checked proofs.
 
 This package provides the `coqidetop` language server, an
 implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
-which allows clients, such as CoqIDE, to interact with Coq in a
+which allows clients, such as RocqIDE, to interact with Coq in a
 structured way."))
 
 (package
- (name coqide)
+ (name rocqide)
  (depends
   (ocamlfind :build)
   (conf-findutils :build)
@@ -106,7 +106,7 @@ a formal language to write mathematical definitions, executable
 algorithms and theorems together with an environment for
 semi-interactive development of machine-checked proofs.
 
-This package provides the CoqIDE, a graphical user interface for the
+This package provides the RocqIDE, a graphical user interface for the
 development of interactive proofs."))
 
 (package
diff --git a/ide/coqide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang
deleted file mode 100644
index d71277f42cc1f..0000000000000
--- a/ide/coqide/coq-ssreflect.lang
+++ /dev/null
@@ -1,249 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<language id="coq-ssreflect" _name="Coq + Ssreflect" version="2.0" _section="Scientific">
-  <metadata>
-    <property name="globs">*.v</property>
-    <property name="block-comment-start">\(\*</property>
-    <property name="block-comment-stop">\*\)</property>
-  </metadata>
-  
-  <styles>
-    <style id="comment" _name="Comment" map-to="def:comment"/>
-    <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/>
-    <style id="vernac-keyword" _name="Vernacular keyword" map-to="def:keyword"/>
-    <style id="gallina-keyword" _name="Gallina keyword" map-to="def:keyword"/>
-    <style id="identifier" _name="Identifier" map-to="def:identifier"/>
-    <style id="constr-keyword" _name="Cic keyword" map-to="def:keyword"/>
-    <style id="constr-sort" _name="Cic sort" map-to="def:builtin"/>
-    <style id="string" _name="String" map-to="def:string"/>
-    <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
-    <style id="error" _name="Error" map-to="def:error"/>
-    <style id="safe" _name="Checked Part"/>
-    <style id="sentence" _name="Sentence terminator"/>
-    <style id="tactic" _name="Tactic"/>
-    <style id="endtactic" _name="Tactic terminator"/>
-    <style id="iterator" _name="Tactic iterator"/>
-  </styles>
-  
-  <definitions>
-    <define-regex id="space">\s</define-regex>
-    <define-regex id="first_ident_char">[_\p{L}]</define-regex>
-    <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
-    <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
-    <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex>
-    <define-regex id="undotted_sep">[-+*{}]</define-regex>
-    <define-regex id="dot_sep">\.(\s|\z)</define-regex>
-    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Variant)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
-    <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
-    <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
-    <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
-    <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex>
-    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))</define-regex>
-
-    <context id="escape-seq" style-ref="escape">
-      <match>""</match>
-    </context>
-    <context id="string" style-ref="string">
-      <start>"</start>
-      <end>"</end>
-      <include>
-	<context ref="escape-seq"/>
-      </include>
-    </context>
-    <context id="ssr-iter" style-ref="iterator">
-      <keyword>do</keyword>
-      <keyword>last</keyword>
-      <keyword>first</keyword>
-    </context>
-    <context id="ssr-tac" style-ref="tactic">
-      <keyword>apply</keyword>
-      <keyword>auto</keyword>
-      <keyword>case</keyword>
-      <keyword>case</keyword>
-      <keyword>congr</keyword>
-      <keyword>elim</keyword>
-      <keyword>exists</keyword>
-      <keyword>have</keyword>
-      <keyword>gen have</keyword>
-      <keyword>generally have</keyword>
-      <keyword>move</keyword>
-      <keyword>pose</keyword>
-      <keyword>rewrite</keyword>
-      <keyword>set</keyword>
-      <keyword>split</keyword>
-      <keyword>suffices</keyword>
-      <keyword>suff</keyword>
-      <keyword>transitivity</keyword>
-      <keyword>under</keyword>
-      <keyword>without loss</keyword>
-      <keyword>wlog</keyword>
-    </context>
-    <context id="ssr-endtac" style-ref="endtactic">
-      <keyword>by</keyword>
-      <keyword>over</keyword>
-      <keyword>exact</keyword>
-      <keyword>reflexivity</keyword>
-    </context>
-    <context id="coq-ssreflect" class="no-spell-check">
-      <include>
-        <context ref="string"/>
-	<context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check">
-	  <start>\(\*\*(\s|\z)</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context ref="comment-in-comment"/>
-	    <context ref="string"/>
-	    <context ref="escape-seq"/>
-	  </include>
-	</context>
-	<context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
-	  <start>\(\*</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
-	      <start>\(\*</start>
-	      <end>\*\)</end>
-	      <include>
-		<context ref="comment-in-comment"/>
-		<context ref="string"/>
-		<context ref="escape-seq"/>
-	      </include>
-	    </context>
-	    <context ref="string"/>
-	    <context ref="escape-seq"/>
-	  </include>
-	</context>
-	<context id="declaration">
-	  <start>\%{decl_head}</start>
-	  <end>\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="id" where="start" style-ref="identifier"/>
-	    <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
-	    <context sub-pattern="id_list" where="start" style-ref="identifier"/>
-	    <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
-	    <context id="constr-keyword" style-ref="constr-keyword">
-	      <keyword>forall</keyword>
-	      <keyword>fun</keyword>
-	      <keyword>match</keyword>
-	      <keyword>fix</keyword>
-	      <keyword>cofix</keyword>
-	      <keyword>with</keyword>
-	      <keyword>for</keyword>
-	      <keyword>end</keyword>
-	      <keyword>as</keyword>
-	      <keyword>let</keyword>
-	      <keyword>in</keyword>
-	      <keyword>if</keyword>
-	      <keyword>then</keyword>
-	      <keyword>else</keyword>
-	      <keyword>return</keyword>
-	      <keyword>using</keyword>
-	    </context>
-	    <context id="constr-sort" style-ref="constr-sort">
-	      <keyword>Prop</keyword>
-	      <keyword>Set</keyword>
-	      <keyword>Type</keyword>
-	    </context>
-	    <context id="dot-nosep">
-	      <match>\.\.</match>
-	    </context>
-	    <context ref="comment"/>
-	    <context ref="string"/>
-	    <context ref="coqdoc"/>
-	  </include>
-	</context>
-	<context id="proof">
-	  <start>Proof</start>
-	  <end>\%{end_proof}\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-	    <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
-	    <context ref="command"/>
-	    <context ref="scope-command"/>
-	    <context ref="hint-command"/>
-	    <context ref="command-for-qualit"/>
-	    <context ref="declaration"/>
-	    <context ref="comment"/>
-	    <context ref="string"/>
-	    <context ref="coqdoc"/>
-	    <context ref="proof"/>
-	    <context ref="undotted-sep"/>
-	    <context id="tactic" extend-parent="false">
-              <start></start>
-              <end>\%{dot_sep}</end>
-	      <include>
-	        <context ref="ssr-tac"/>
-	        <context ref="ssr-endtac"/>
-	        <context ref="ssr-iter"/>
-		<context ref="dot-nosep"/>
-		<context ref="constr-keyword"/>
-		<context ref="constr-sort"/>
-	        <context ref="comment"/>
-	        <context ref="string"/>
-	      </include>
-	    </context>
-	  </include>
-	</context>
-	<context id="undotted-sep" style-ref="vernac-keyword">
-	  <match>\%{undotted_sep}</match>
-	</context>
-	<context id="command" style-ref="vernac-keyword">
-	  <keyword>Add</keyword>
-	  <keyword>Check</keyword>
-	  <keyword>Eval</keyword>
-	  <keyword>Load</keyword>
-	  <keyword>Undo</keyword>
-          <keyword>Restart</keyword>
-	  <keyword>Goal</keyword>
-	  <keyword>Print</keyword>
-	  <keyword>Save</keyword>
-	  <keyword>Comments</keyword>
-	  <keyword>Solve\%{space}+Obligation</keyword>
-	  <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword>
-	  <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
-	  <keyword>\%{locality}Infix</keyword>
-	  <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
-	</context>
-	<context id="hint-command" style-ref="vernac-keyword">
-	  <prefix>\%{locality}Hint\%{space}+</prefix>
-	  <keyword>Resolve</keyword>
-	  <keyword>Immediate</keyword>
-	  <keyword>Constructors</keyword>
-	  <keyword>unfold</keyword>
-	  <keyword>Opaque</keyword>
-	  <keyword>Transparent</keyword>
-	  <keyword>Extern</keyword>
-	</context>
-	<context id="scope-command" style-ref="vernac-keyword">
-	  <suffix>\%{space}+Scope</suffix>
-	  <keyword>\%{locality}Open</keyword>
-	  <keyword>\%{locality}Close</keyword>
-	  <keyword>Bind</keyword>
-	  <keyword>Delimit</keyword>
-	</context>
-	<context id="command-for-qualit">
-	  <suffix>\%{space}+(?'qua'\%{qualit})</suffix>
-	  <keyword>Chapter</keyword>
-	  <keyword>Combined\%{space}+Scheme</keyword>
-	  <keyword>End</keyword>
-	  <keyword>Section</keyword>
-	  <keyword>Arguments</keyword>
-	  <keyword>Implicit\%{space}+Arguments</keyword>
-	  <keyword>(Import)|(Include)</keyword>
-	  <keyword>Require(\%{space}+((Import)|(Export)))?</keyword>
-          <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(OCaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword>
-	  <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword>
-	  <include>
-	    <context sub-pattern="1" style-ref="vernac-keyword"/>
-	  </include>
-	</context>
-	<context id="command-for-qualit-list" style-ref="vernac-keyword">
-	  <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix>
-	  <keyword>Typeclasses (Transparent)|(Opaque)</keyword>
-	  <include>
-	    <context sub-pattern="qua_list" style-ref="identifier"/>
-	  </include>
-	</context>
-      </include>
-    </context>
-  </definitions>
-</language>
diff --git a/ide/coqide/coq_icon.rc b/ide/coqide/coq_icon.rc
deleted file mode 100644
index 3e8b8aaecc99e..0000000000000
--- a/ide/coqide/coq_icon.rc
+++ /dev/null
@@ -1 +0,0 @@
-large   ICON    ide/coqide/coq.ico
diff --git a/ide/coqide/index.mld b/ide/coqide/index.mld
deleted file mode 100644
index 8852a2a7ebad4..0000000000000
--- a/ide/coqide/index.mld
+++ /dev/null
@@ -1,3 +0,0 @@
-{0 coqide }
-
-The coqide package only contains the CoqIDE executable and no OCaml library.
diff --git a/ide/coqide/FAQ b/ide/rocqide/FAQ
similarity index 91%
rename from ide/coqide/FAQ
rename to ide/rocqide/FAQ
index 3e23f444b74dc..79689eabc29b9 100644
--- a/ide/coqide/FAQ
+++ b/ide/rocqide/FAQ
@@ -1,8 +1,8 @@
-			CoqIDE FAQ
+			RocqIDE FAQ
 
 TODO: Put the relevant info in the doc and delete this file.
 
-Q0) What is CoqIDE?
+Q0) What is RocqIDE?
 R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations.
 
 Q1) How to enable Emacs keybindings?
@@ -22,12 +22,12 @@ R4) Thanks to the Notation features in Coq, you just need to insert these
 Notation "∀ x : t, P" := (forall x:t, P) (at level 200, x ident).
 Notation "∃ x : t, P" := (exists x:t, P) (at level 200, x ident).
 ======================================================================
-Copy/Paste of these lines from this file will not work outside of CoqIDE.
+Copy/Paste of these lines from this file will not work outside of RocqIDE.
 You need to load a file containing these lines or to enter the "∀" 
 using an input method (see Q5). To try it just use "Require utf8" from inside
-CoqIDE. 
-To enable these notations automatically start coqide with
-	coqide -l utf8
+RocqIDE. 
+To enable these notations automatically start rocqide with
+	rocqide -l utf8
 In the ide subdir of Coq library, you will find a sample utf8.v with some 
 pretty simple notations.
 
@@ -42,7 +42,7 @@ a module for LaTeX-like inputting.
 Q6) How to customize the shortcuts for menus?
 R6) Two solutions are offered:
   - Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or
-  - If your system allows it, from CoqIDE, you may select a menu entry and press the 
+  - If your system allows it, from RocqIDE, you may select a menu entry and press the 
     desired shortcut. 
 
 Q7) What encoding should I use? What is this \x{iiii} in my file?
diff --git a/ide/coqide/MacOS/coqfile.icns b/ide/rocqide/MacOS/coqfile.icns
similarity index 100%
rename from ide/coqide/MacOS/coqfile.icns
rename to ide/rocqide/MacOS/coqfile.icns
diff --git a/ide/coqide/MacOS/coqide.icns b/ide/rocqide/MacOS/coqide.icns
similarity index 100%
rename from ide/coqide/MacOS/coqide.icns
rename to ide/rocqide/MacOS/coqide.icns
diff --git a/ide/coqide/Make b/ide/rocqide/Make
similarity index 100%
rename from ide/coqide/Make
rename to ide/rocqide/Make
diff --git a/ide/coqide/config.mli b/ide/rocqide/config.mli
similarity index 100%
rename from ide/coqide/config.mli
rename to ide/rocqide/config.mli
diff --git a/ide/coqide/config_lexer.mli b/ide/rocqide/config_lexer.mli
similarity index 100%
rename from ide/coqide/config_lexer.mli
rename to ide/rocqide/config_lexer.mli
diff --git a/ide/coqide/config_lexer.mll b/ide/rocqide/config_lexer.mll
similarity index 82%
rename from ide/coqide/config_lexer.mll
rename to ide/rocqide/config_lexer.mll
index f151277a2b073..9a22ee670d3db 100644
--- a/ide/coqide/config_lexer.mll
+++ b/ide/rocqide/config_lexer.mll
@@ -24,18 +24,18 @@ let ignore = space | ('#' [^ '\n']*)
 
 rule prefs m = parse
   |ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
-				 prefs (Util.String.Map.add id conf m) lexbuf }
+                                 prefs (Util.String.Map.add id conf m) lexbuf }
   | _     { let c = lexeme_start lexbuf in
-	      eprintf "coqiderc: invalid character (%d)\n@." c;
-	      prefs m lexbuf }
+              eprintf "coqiderc: invalid character (%d)\n@." c;
+              prefs m lexbuf }
   | eof   { m }
 
 and str_list l = parse
   | ignore* '"'   { Buffer.reset string_buffer;
-		    Buffer.add_char string_buffer '"';
-		    string lexbuf;
-		    let s = Buffer.contents string_buffer in
-		      str_list ((Scanf.sscanf s "%S" (fun s -> s))::l) lexbuf }
+                    Buffer.add_char string_buffer '"';
+                    string lexbuf;
+                    let s = Buffer.contents string_buffer in
+                      str_list ((Scanf.sscanf s "%S" (fun s -> s))::l) lexbuf }
   |ignore+ { List.rev l}
 
 and string = parse
diff --git a/ide/rocqide/coq-ssreflect.lang b/ide/rocqide/coq-ssreflect.lang
new file mode 100644
index 0000000000000..37a9f9a1d96f4
--- /dev/null
+++ b/ide/rocqide/coq-ssreflect.lang
@@ -0,0 +1,249 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<language id="coq-ssreflect" _name="Coq + Ssreflect" version="2.0" _section="Scientific">
+  <metadata>
+    <property name="globs">*.v</property>
+    <property name="block-comment-start">\(\*</property>
+    <property name="block-comment-stop">\*\)</property>
+  </metadata>
+
+  <styles>
+    <style id="comment" _name="Comment" map-to="def:comment"/>
+    <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/>
+    <style id="vernac-keyword" _name="Vernacular keyword" map-to="def:keyword"/>
+    <style id="gallina-keyword" _name="Gallina keyword" map-to="def:keyword"/>
+    <style id="identifier" _name="Identifier" map-to="def:identifier"/>
+    <style id="constr-keyword" _name="Cic keyword" map-to="def:keyword"/>
+    <style id="constr-sort" _name="Cic sort" map-to="def:builtin"/>
+    <style id="string" _name="String" map-to="def:string"/>
+    <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
+    <style id="error" _name="Error" map-to="def:error"/>
+    <style id="safe" _name="Checked Part"/>
+    <style id="sentence" _name="Sentence terminator"/>
+    <style id="tactic" _name="Tactic"/>
+    <style id="endtactic" _name="Tactic terminator"/>
+    <style id="iterator" _name="Tactic iterator"/>
+  </styles>
+
+  <definitions>
+    <define-regex id="space">\s</define-regex>
+    <define-regex id="first_ident_char">[_\p{L}]</define-regex>
+    <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
+    <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
+    <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex>
+    <define-regex id="undotted_sep">[-+*{}]</define-regex>
+    <define-regex id="dot_sep">\.(\s|\z)</define-regex>
+    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Variant)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
+    <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
+    <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
+    <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
+    <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex>
+    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))</define-regex>
+
+    <context id="escape-seq" style-ref="escape">
+      <match>""</match>
+    </context>
+    <context id="string" style-ref="string">
+      <start>"</start>
+      <end>"</end>
+      <include>
+        <context ref="escape-seq"/>
+      </include>
+    </context>
+    <context id="ssr-iter" style-ref="iterator">
+      <keyword>do</keyword>
+      <keyword>last</keyword>
+      <keyword>first</keyword>
+    </context>
+    <context id="ssr-tac" style-ref="tactic">
+      <keyword>apply</keyword>
+      <keyword>auto</keyword>
+      <keyword>case</keyword>
+      <keyword>case</keyword>
+      <keyword>congr</keyword>
+      <keyword>elim</keyword>
+      <keyword>exists</keyword>
+      <keyword>have</keyword>
+      <keyword>gen have</keyword>
+      <keyword>generally have</keyword>
+      <keyword>move</keyword>
+      <keyword>pose</keyword>
+      <keyword>rewrite</keyword>
+      <keyword>set</keyword>
+      <keyword>split</keyword>
+      <keyword>suffices</keyword>
+      <keyword>suff</keyword>
+      <keyword>transitivity</keyword>
+      <keyword>under</keyword>
+      <keyword>without loss</keyword>
+      <keyword>wlog</keyword>
+    </context>
+    <context id="ssr-endtac" style-ref="endtactic">
+      <keyword>by</keyword>
+      <keyword>over</keyword>
+      <keyword>exact</keyword>
+      <keyword>reflexivity</keyword>
+    </context>
+    <context id="coq-ssreflect" class="no-spell-check">
+      <include>
+        <context ref="string"/>
+        <context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check">
+          <start>\(\*\*(\s|\z)</start>
+          <end>\*\)</end>
+          <include>
+            <context ref="comment-in-comment"/>
+            <context ref="string"/>
+            <context ref="escape-seq"/>
+          </include>
+        </context>
+        <context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
+          <start>\(\*</start>
+          <end>\*\)</end>
+          <include>
+            <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
+              <start>\(\*</start>
+              <end>\*\)</end>
+              <include>
+                <context ref="comment-in-comment"/>
+                <context ref="string"/>
+                <context ref="escape-seq"/>
+              </include>
+            </context>
+            <context ref="string"/>
+            <context ref="escape-seq"/>
+          </include>
+        </context>
+        <context id="declaration">
+          <start>\%{decl_head}</start>
+          <end>\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="id" where="start" style-ref="identifier"/>
+            <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
+            <context sub-pattern="id_list" where="start" style-ref="identifier"/>
+            <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
+            <context id="constr-keyword" style-ref="constr-keyword">
+              <keyword>forall</keyword>
+              <keyword>fun</keyword>
+              <keyword>match</keyword>
+              <keyword>fix</keyword>
+              <keyword>cofix</keyword>
+              <keyword>with</keyword>
+              <keyword>for</keyword>
+              <keyword>end</keyword>
+              <keyword>as</keyword>
+              <keyword>let</keyword>
+              <keyword>in</keyword>
+              <keyword>if</keyword>
+              <keyword>then</keyword>
+              <keyword>else</keyword>
+              <keyword>return</keyword>
+              <keyword>using</keyword>
+            </context>
+            <context id="constr-sort" style-ref="constr-sort">
+              <keyword>Prop</keyword>
+              <keyword>Set</keyword>
+              <keyword>Type</keyword>
+            </context>
+            <context id="dot-nosep">
+              <match>\.\.</match>
+            </context>
+            <context ref="comment"/>
+            <context ref="string"/>
+            <context ref="coqdoc"/>
+          </include>
+        </context>
+        <context id="proof">
+          <start>Proof</start>
+          <end>\%{end_proof}\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
+            <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
+            <context ref="command"/>
+            <context ref="scope-command"/>
+            <context ref="hint-command"/>
+            <context ref="command-for-qualit"/>
+            <context ref="declaration"/>
+            <context ref="comment"/>
+            <context ref="string"/>
+            <context ref="coqdoc"/>
+            <context ref="proof"/>
+            <context ref="undotted-sep"/>
+            <context id="tactic" extend-parent="false">
+              <start></start>
+              <end>\%{dot_sep}</end>
+              <include>
+                <context ref="ssr-tac"/>
+                <context ref="ssr-endtac"/>
+                <context ref="ssr-iter"/>
+                <context ref="dot-nosep"/>
+                <context ref="constr-keyword"/>
+                <context ref="constr-sort"/>
+                <context ref="comment"/>
+                <context ref="string"/>
+              </include>
+            </context>
+          </include>
+        </context>
+        <context id="undotted-sep" style-ref="vernac-keyword">
+          <match>\%{undotted_sep}</match>
+        </context>
+        <context id="command" style-ref="vernac-keyword">
+          <keyword>Add</keyword>
+          <keyword>Check</keyword>
+          <keyword>Eval</keyword>
+          <keyword>Load</keyword>
+          <keyword>Undo</keyword>
+          <keyword>Restart</keyword>
+          <keyword>Goal</keyword>
+          <keyword>Print</keyword>
+          <keyword>Save</keyword>
+          <keyword>Comments</keyword>
+          <keyword>Solve\%{space}+Obligation</keyword>
+          <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword>
+          <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
+          <keyword>\%{locality}Infix</keyword>
+          <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
+        </context>
+        <context id="hint-command" style-ref="vernac-keyword">
+          <prefix>\%{locality}Hint\%{space}+</prefix>
+          <keyword>Resolve</keyword>
+          <keyword>Immediate</keyword>
+          <keyword>Constructors</keyword>
+          <keyword>unfold</keyword>
+          <keyword>Opaque</keyword>
+          <keyword>Transparent</keyword>
+          <keyword>Extern</keyword>
+        </context>
+        <context id="scope-command" style-ref="vernac-keyword">
+          <suffix>\%{space}+Scope</suffix>
+          <keyword>\%{locality}Open</keyword>
+          <keyword>\%{locality}Close</keyword>
+          <keyword>Bind</keyword>
+          <keyword>Delimit</keyword>
+        </context>
+        <context id="command-for-qualit">
+          <suffix>\%{space}+(?'qua'\%{qualit})</suffix>
+          <keyword>Chapter</keyword>
+          <keyword>Combined\%{space}+Scheme</keyword>
+          <keyword>End</keyword>
+          <keyword>Section</keyword>
+          <keyword>Arguments</keyword>
+          <keyword>Implicit\%{space}+Arguments</keyword>
+          <keyword>(Import)|(Include)</keyword>
+          <keyword>Require(\%{space}+((Import)|(Export)))?</keyword>
+          <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(OCaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword>
+          <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword>
+          <include>
+            <context sub-pattern="1" style-ref="vernac-keyword"/>
+          </include>
+        </context>
+        <context id="command-for-qualit-list" style-ref="vernac-keyword">
+          <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix>
+          <keyword>Typeclasses (Transparent)|(Opaque)</keyword>
+          <include>
+            <context sub-pattern="qua_list" style-ref="identifier"/>
+          </include>
+        </context>
+      </include>
+    </context>
+  </definitions>
+</language>
diff --git a/ide/coqide/coq.ico b/ide/rocqide/coq.ico
similarity index 100%
rename from ide/coqide/coq.ico
rename to ide/rocqide/coq.ico
diff --git a/ide/coqide/coq.lang b/ide/rocqide/coq.lang
similarity index 100%
rename from ide/coqide/coq.lang
rename to ide/rocqide/coq.lang
diff --git a/ide/coqide/coq.png b/ide/rocqide/coq.png
similarity index 100%
rename from ide/coqide/coq.png
rename to ide/rocqide/coq.png
diff --git a/ide/coqide/coq2.ico b/ide/rocqide/coq2.ico
similarity index 100%
rename from ide/coqide/coq2.ico
rename to ide/rocqide/coq2.ico
diff --git a/ide/rocqide/coq_icon.rc b/ide/rocqide/coq_icon.rc
new file mode 100644
index 0000000000000..53898a7258d88
--- /dev/null
+++ b/ide/rocqide/coq_icon.rc
@@ -0,0 +1 @@
+large   ICON    ide/rocqide/coq.ico
diff --git a/ide/coqide/coq_style.xml b/ide/rocqide/coq_style.xml
similarity index 96%
rename from ide/coqide/coq_style.xml
rename to ide/rocqide/coq_style.xml
index 00251d89bad2f..aeb3a32235b8e 100644
--- a/ide/coqide/coq_style.xml
+++ b/ide/rocqide/coq_style.xml
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <style-scheme id="coq_style" _name="Coq style"
-	      parent-scheme="classic" version="1.0">
+              parent-scheme="classic" version="1.0">
 <author>The Coq Dev Team</author>
 <_description>Coq/Ssreflect color scheme for the vernacular language</_description>
 
diff --git a/ide/coqide/default_bindings_src.ml b/ide/rocqide/default_bindings_src.ml
similarity index 100%
rename from ide/coqide/default_bindings_src.ml
rename to ide/rocqide/default_bindings_src.ml
diff --git a/ide/coqide/default_bindings_src.mli b/ide/rocqide/default_bindings_src.mli
similarity index 100%
rename from ide/coqide/default_bindings_src.mli
rename to ide/rocqide/default_bindings_src.mli
diff --git a/ide/coqide/document.ml b/ide/rocqide/document.ml
similarity index 100%
rename from ide/coqide/document.ml
rename to ide/rocqide/document.ml
diff --git a/ide/coqide/document.mli b/ide/rocqide/document.mli
similarity index 100%
rename from ide/coqide/document.mli
rename to ide/rocqide/document.mli
diff --git a/ide/coqide/dune b/ide/rocqide/dune
similarity index 91%
rename from ide/coqide/dune
rename to ide/rocqide/dune
index d0d6de07fe060..f24e2c1dde447 100644
--- a/ide/coqide/dune
+++ b/ide/rocqide/dune
@@ -18,7 +18,7 @@
 
 ; IDE Client, we may want to add the macos_prehook.ml conditionally.
 (library
- (name coqide_gui)
+ (name rocqide_gui)
  (wrapped false)
  (modules (:standard \ document idetop rocqide_main default_bindings_src gen_gtk_platform
     shared shared_os_specific))
@@ -63,14 +63,14 @@
 
 (executable
  (name rocqide_main)
- (public_name coqide)
- (package coqide)
+ (public_name rocqide)
+ (package rocqide)
  (modules rocqide_main)
  (modes exe byte)
- (libraries coqide_gui))
+ (libraries rocqide_gui))
 
 (documentation
- (package coqide))
+ (package rocqide))
 
 ; Input-method bindings
 (executable
@@ -82,11 +82,11 @@
  (deps (:gen ./default_bindings_src.exe))
  (action (run %{gen} %{targets})))
 
-; FIXME: we should install those in share/coqide. We better do this
+; FIXME: we should install those in share/rocqide. We better do this
 ; once the make-based system has been phased out.
 (install
  (section share_root)
- (package coqide)
+ (package rocqide)
  (files
   (coq.png as coq/coq.png)
   (default.bindings as coq/default.bindings)
diff --git a/ide/coqide/fileOps.ml b/ide/rocqide/fileOps.ml
similarity index 100%
rename from ide/coqide/fileOps.ml
rename to ide/rocqide/fileOps.ml
diff --git a/ide/coqide/fileOps.mli b/ide/rocqide/fileOps.mli
similarity index 100%
rename from ide/coqide/fileOps.mli
rename to ide/rocqide/fileOps.mli
diff --git a/ide/coqide/gen_gtk_platform.ml b/ide/rocqide/gen_gtk_platform.ml
similarity index 100%
rename from ide/coqide/gen_gtk_platform.ml
rename to ide/rocqide/gen_gtk_platform.ml
diff --git a/ide/coqide/gen_gtk_platform.mli b/ide/rocqide/gen_gtk_platform.mli
similarity index 100%
rename from ide/coqide/gen_gtk_platform.mli
rename to ide/rocqide/gen_gtk_platform.mli
diff --git a/ide/coqide/gtk_parsing.ml b/ide/rocqide/gtk_parsing.ml
similarity index 100%
rename from ide/coqide/gtk_parsing.ml
rename to ide/rocqide/gtk_parsing.ml
diff --git a/ide/coqide/gtk_parsing.mli b/ide/rocqide/gtk_parsing.mli
similarity index 100%
rename from ide/coqide/gtk_parsing.mli
rename to ide/rocqide/gtk_parsing.mli
diff --git a/ide/coqide/idetop.ml b/ide/rocqide/idetop.ml
similarity index 99%
rename from ide/coqide/idetop.ml
rename to ide/rocqide/idetop.ml
index 593f6880de163..cc123e71267ac 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/rocqide/idetop.ml
@@ -694,7 +694,7 @@ let islave_parse opts extra_args =
   let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra opts extra_args in
   let extra_args = parse extra_args in
   (* One of the role of coqidetop is to find the name of buffers to open *)
-  (* in the command line; Coqide is waiting these names on stdout *)
+  (* in the command line; Rocqide is waiting these names on stdout *)
   (* (see filter_rocq_opts in rocq.ml), so we send them now *)
   print_string (String.concat "\n" extra_args);
   ( { Coqtop.run_mode; color_mode }, stm_opts), []
diff --git a/ide/coqide/idetop.mli b/ide/rocqide/idetop.mli
similarity index 100%
rename from ide/coqide/idetop.mli
rename to ide/rocqide/idetop.mli
diff --git a/ide/coqide/ideutils.ml b/ide/rocqide/ideutils.ml
similarity index 99%
rename from ide/coqide/ideutils.ml
rename to ide/rocqide/ideutils.ml
index 420db81ab8d57..2fc6644951612 100644
--- a/ide/coqide/ideutils.ml
+++ b/ide/rocqide/ideutils.ml
@@ -462,7 +462,7 @@ let stat f =
 
 (** I/O utilities
 
-    Note: In a mono-thread coqide, we use the same buffer for
+    Note: In a mono-thread rocqide, we use the same buffer for
     different read operations *)
 
 let maxread = 4096
diff --git a/ide/coqide/ideutils.mli b/ide/rocqide/ideutils.mli
similarity index 100%
rename from ide/coqide/ideutils.mli
rename to ide/rocqide/ideutils.mli
diff --git a/ide/rocqide/index.mld b/ide/rocqide/index.mld
new file mode 100644
index 0000000000000..1cf996cf5d25c
--- /dev/null
+++ b/ide/rocqide/index.mld
@@ -0,0 +1,3 @@
+{0 rocqide }
+
+The rocqide package only contains the RocqIDE executable and no OCaml library.
diff --git a/ide/coqide/macos_prehook.ml b/ide/rocqide/macos_prehook.ml
similarity index 100%
rename from ide/coqide/macos_prehook.ml
rename to ide/rocqide/macos_prehook.ml
diff --git a/ide/coqide/macos_prehook.mli b/ide/rocqide/macos_prehook.mli
similarity index 100%
rename from ide/coqide/macos_prehook.mli
rename to ide/rocqide/macos_prehook.mli
diff --git a/ide/coqide/microPG.ml b/ide/rocqide/microPG.ml
similarity index 100%
rename from ide/coqide/microPG.ml
rename to ide/rocqide/microPG.ml
diff --git a/ide/coqide/microPG.mli b/ide/rocqide/microPG.mli
similarity index 100%
rename from ide/coqide/microPG.mli
rename to ide/rocqide/microPG.mli
diff --git a/ide/coqide/minilib.ml b/ide/rocqide/minilib.ml
similarity index 100%
rename from ide/coqide/minilib.ml
rename to ide/rocqide/minilib.ml
diff --git a/ide/coqide/minilib.mli b/ide/rocqide/minilib.mli
similarity index 100%
rename from ide/coqide/minilib.mli
rename to ide/rocqide/minilib.mli
diff --git a/ide/coqide/preferences.ml b/ide/rocqide/preferences.ml
similarity index 98%
rename from ide/coqide/preferences.ml
rename to ide/rocqide/preferences.ml
index 4df579cc82412..d4bae70cb552a 100644
--- a/ide/coqide/preferences.ml
+++ b/ide/rocqide/preferences.ml
@@ -371,12 +371,7 @@ let modifiers_valid =
    (* Note: <Primary> is providing <Meta> (i.e. "Command") for Darwin, i.e. MacOS X *)
     ~init:"<Alt><Control><Shift><Primary>" ~repr:Repr.(string)
 
-let browser_cmd_fmt =
- try
-  let rocq_netscape_remote_var = "COQREMOTEBROWSER" in
-  Sys.getenv rocq_netscape_remote_var
- with
-  Not_found -> Coq_config.browser
+let browser_cmd_fmt = Option.default Coq_config.browser (Boot.Util.getenv_rocq "REMOTEBROWSER")
 
 let cmd_browse =
   new preference ~name:["cmd_browse"] ~init:browser_cmd_fmt ~repr:Repr.(string)
@@ -689,10 +684,10 @@ let load_pref_file loader warn name =
     warn ~delay:5000 ("No user " ^ name ^ ", using system wide configuration");
     try_load_pref_file loader warn system_wide_file
   with Not_found ->
-  (* Compatibility with oldest versions of CoqIDE (<= 8.4) *)
+  (* Compatibility with oldest versions of RocqIDE (<= 8.4) *)
   try
     let old_user_file = get_config_file [Option.default "" (Glib.get_home_dir ())] ("."^name) in
-    warn ~delay:5000 ("No " ^ name ^ ", trying to recover from an older version of CoqIDE");
+    warn ~delay:5000 ("No " ^ name ^ ", trying to recover from an older version of RocqIDE");
     try_load_pref_file loader warn old_user_file
   with Not_found ->
   (* Built-in configuration *)
diff --git a/ide/coqide/preferences.mli b/ide/rocqide/preferences.mli
similarity index 100%
rename from ide/coqide/preferences.mli
rename to ide/rocqide/preferences.mli
diff --git a/ide/coqide/preferences_ui.ml b/ide/rocqide/preferences_ui.ml
similarity index 100%
rename from ide/coqide/preferences_ui.ml
rename to ide/rocqide/preferences_ui.ml
diff --git a/ide/coqide/preferences_ui.mli b/ide/rocqide/preferences_ui.mli
similarity index 100%
rename from ide/coqide/preferences_ui.mli
rename to ide/rocqide/preferences_ui.mli
diff --git a/ide/coqide/protocol/dune b/ide/rocqide/protocol/dune
similarity index 100%
rename from ide/coqide/protocol/dune
rename to ide/rocqide/protocol/dune
diff --git a/ide/coqide/protocol/interface.mli b/ide/rocqide/protocol/interface.mli
similarity index 98%
rename from ide/coqide/protocol/interface.mli
rename to ide/rocqide/protocol/interface.mli
index a6d2bf924563b..e1e9187b12e7b 100644
--- a/ide/coqide/protocol/interface.mli
+++ b/ide/rocqide/protocol/interface.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** * Declarative part of the interface of CoqIDE calls to Rocq *)
+(** * Declarative part of the interface of RocqIDE calls to Rocq *)
 
 (** * Generic structures *)
 
@@ -148,7 +148,7 @@ type 'a value =
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
-(* Request/Reply message protocol between Rocq and CoqIDE *)
+(* Request/Reply message protocol between Rocq and RocqIDE *)
 
 (**  [add ((((s,eid),(sid,v)), bp), (line_nb, bol_pos) ] adds the phrase [s] with edit id [eid]
      on top of the current edit position (that is asserted to be [sid]).
diff --git a/ide/coqide/protocol/richpp.ml b/ide/rocqide/protocol/richpp.ml
similarity index 100%
rename from ide/coqide/protocol/richpp.ml
rename to ide/rocqide/protocol/richpp.ml
diff --git a/ide/coqide/protocol/richpp.mli b/ide/rocqide/protocol/richpp.mli
similarity index 100%
rename from ide/coqide/protocol/richpp.mli
rename to ide/rocqide/protocol/richpp.mli
diff --git a/ide/coqide/protocol/serialize.ml b/ide/rocqide/protocol/serialize.ml
similarity index 100%
rename from ide/coqide/protocol/serialize.ml
rename to ide/rocqide/protocol/serialize.ml
diff --git a/ide/coqide/protocol/serialize.mli b/ide/rocqide/protocol/serialize.mli
similarity index 100%
rename from ide/coqide/protocol/serialize.mli
rename to ide/rocqide/protocol/serialize.mli
diff --git a/ide/coqide/protocol/xml_lexer.mli b/ide/rocqide/protocol/xml_lexer.mli
similarity index 100%
rename from ide/coqide/protocol/xml_lexer.mli
rename to ide/rocqide/protocol/xml_lexer.mli
diff --git a/ide/coqide/protocol/xml_lexer.mll b/ide/rocqide/protocol/xml_lexer.mll
similarity index 100%
rename from ide/coqide/protocol/xml_lexer.mll
rename to ide/rocqide/protocol/xml_lexer.mll
diff --git a/ide/coqide/protocol/xml_parser.ml b/ide/rocqide/protocol/xml_parser.ml
similarity index 100%
rename from ide/coqide/protocol/xml_parser.ml
rename to ide/rocqide/protocol/xml_parser.ml
diff --git a/ide/coqide/protocol/xml_parser.mli b/ide/rocqide/protocol/xml_parser.mli
similarity index 100%
rename from ide/coqide/protocol/xml_parser.mli
rename to ide/rocqide/protocol/xml_parser.mli
diff --git a/ide/coqide/protocol/xml_printer.ml b/ide/rocqide/protocol/xml_printer.ml
similarity index 100%
rename from ide/coqide/protocol/xml_printer.ml
rename to ide/rocqide/protocol/xml_printer.ml
diff --git a/ide/coqide/protocol/xml_printer.mli b/ide/rocqide/protocol/xml_printer.mli
similarity index 100%
rename from ide/coqide/protocol/xml_printer.mli
rename to ide/rocqide/protocol/xml_printer.mli
diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/rocqide/protocol/xmlprotocol.ml
similarity index 99%
rename from ide/coqide/protocol/xmlprotocol.ml
rename to ide/rocqide/protocol/xmlprotocol.ml
index 185038a3fd7af..65ed4caa2fa09 100644
--- a/ide/coqide/protocol/xmlprotocol.ml
+++ b/ide/rocqide/protocol/xmlprotocol.ml
@@ -17,7 +17,7 @@ let protocol_version = "20240517"
 type msg_format = Richpp of { width : int; depth : int } | Ppcmds
 let msg_format = ref (Richpp { width = 72; depth = max_int })
 
-(** * Interface of calls to Rocq by CoqIDE *)
+(** * Interface of calls to Rocq by RocqIDE *)
 
 open Util
 open Interface
@@ -1152,4 +1152,3 @@ let of_stack frames = of_value (of_list (of_pair of_string (of_option
     (of_pair of_string (of_list of_int))))) (Good frames)
 
 (* vim: set foldmethod=marker: *)
-
diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/rocqide/protocol/xmlprotocol.mli
similarity index 98%
rename from ide/coqide/protocol/xmlprotocol.mli
rename to ide/rocqide/protocol/xmlprotocol.mli
index 0761101d7676b..8a4fb73597d8a 100644
--- a/ide/coqide/protocol/xmlprotocol.mli
+++ b/ide/rocqide/protocol/xmlprotocol.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** * Applicative part of the interface of CoqIDE calls to Coq *)
+(** * Applicative part of the interface of RocqIDE calls to Rocq *)
 
 open Interface
 open Xml_datatype
diff --git a/ide/coqide/rocqDriver.ml b/ide/rocqide/rocqDriver.ml
similarity index 98%
rename from ide/coqide/rocqDriver.ml
rename to ide/rocqide/rocqDriver.ml
index 9f22df3d0e524..d1714f7cf1e8c 100644
--- a/ide/coqide/rocqDriver.ml
+++ b/ide/rocqide/rocqDriver.ml
@@ -220,7 +220,7 @@ type rocqtop = {
   mutable handle : handle;
   mutable status : status;
   mutable stopped_in_debugger : bool;
-  (* i.e., CoqIDE has received a prompt message *)
+  (* i.e., RocqIDE has received a prompt message *)
   mutable do_when_ready : (unit -> unit) Queue.t;
   (* for debug msgs only; functions are called when rocqtop is Ready *)
   mutable basename : string;
@@ -249,15 +249,15 @@ let lift (f : unit -> 'a) : 'a task =
     kill of the pid.
 
            >--ide2top_w--[pipe]--ide2top_r-->
-    coqide                                   rocqtop
+    rocqide                                   rocqtop
            <--top2ide_r--[pipe]--top2ide_w--<
 
     Note: we use Unix.stderr in Unix.create_process to get debug
     messages from the rocqtop's Ide_slave loop.
 
-    NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
+    NB: it's important to close rocqide's descriptors (ide2top_w and top2ide_r)
     in rocqtop. We do this indirectly via [Unix.set_close_on_exec].
-    This way, coqide has the only remaining copies of these descriptors,
+    This way, rocqide has the only remaining copies of these descriptors,
     and closing them later will have visible effects in rocqtop. Cf man 7 pipe :
 
     - If  all file descriptors referring to the write end of a pipe have been
@@ -269,7 +269,7 @@ let lift (f : unit -> 'a) : 'a task =
       then write(2) fails with the error EPIPE.
 
     Symmetrically, rocqtop's descriptors (ide2top_r and top2ide_w) should be
-    closed in coqide.
+    closed in rocqide.
 *)
 
 exception TubeError of string
diff --git a/ide/coqide/rocqDriver.mli b/ide/rocqide/rocqDriver.mli
similarity index 97%
rename from ide/coqide/rocqDriver.mli
rename to ide/rocqide/rocqDriver.mli
index 8882c63abc1b3..296fb92fe0199 100644
--- a/ide/coqide/rocqDriver.mli
+++ b/ide/rocqide/rocqDriver.mli
@@ -27,7 +27,7 @@ type status = New | Ready | Busy | Closed
              It will reject tasks given via [try_grab].
   - Ready  : no current task, accepts new tasks via [try_grab].
   - Busy   : has accepted a task via [init_rocqtop] or [try_grab],
-  - Closed : the coqide buffer has been closed, we discard any further task.
+  - Closed : the rocqide buffer has been closed, we discard any further task.
 *)
 
 type 'a task
@@ -205,13 +205,13 @@ val version : unit -> string
 val filter_rocq_opts : string list -> string list
 (** * Launch a test rocqtop processes, ask for a correct rocqtop if it fails.
     @return the list of arguments that rocqtop did not understand
-    (the files probably ..). This command may terminate coqide in
+    (the files probably ..). This command may terminate rocqide in
     case of trouble.  *)
 
 val check_connection : string list -> unit
 (** Launch a rocqtop with the user args in order to be sure that it works,
     checking in particular that Prelude.vo is found. This command
-    may terminate coqide in case of trouble *)
+    may terminate rocqide in case of trouble *)
 
 val interrupter : (int -> unit) ref
 val breaker : (int -> unit) ref
diff --git a/ide/coqide/rocqOps.ml b/ide/rocqide/rocqOps.ml
similarity index 99%
rename from ide/coqide/rocqOps.ml
rename to ide/rocqide/rocqOps.ml
index 84bd2ad1f7805..efd912a5f9c01 100644
--- a/ide/coqide/rocqOps.ml
+++ b/ide/rocqide/rocqOps.ml
@@ -189,8 +189,8 @@ let c2b (buffer : GText.buffer) (s_byte, s_uni) uni_off =
    from. [CLexer.after] can compute this from the position of the last
    parsed token.
 
-   However, for CoqIDE, we have a huge problem in the sense that
-   CoqIDE will do its own parsing and the locations may not start at
+   However, for RocqIDE, we have a huge problem in the sense that
+   RocqIDE will do its own parsing and the locations may not start at
    the same point. Thus, we need to perform potentially very costly
    char to offset conversion, for that we need the whole buffer.
 *)
diff --git a/ide/coqide/rocqOps.mli b/ide/rocqide/rocqOps.mli
similarity index 100%
rename from ide/coqide/rocqOps.mli
rename to ide/rocqide/rocqOps.mli
diff --git a/ide/coqide/rocq_commands.ml b/ide/rocqide/rocq_commands.ml
similarity index 100%
rename from ide/coqide/rocq_commands.ml
rename to ide/rocqide/rocq_commands.ml
diff --git a/ide/coqide/rocq_commands.mli b/ide/rocqide/rocq_commands.mli
similarity index 100%
rename from ide/coqide/rocq_commands.mli
rename to ide/rocqide/rocq_commands.mli
diff --git a/ide/coqide/rocq_lex.mli b/ide/rocqide/rocq_lex.mli
similarity index 100%
rename from ide/coqide/rocq_lex.mli
rename to ide/rocqide/rocq_lex.mli
diff --git a/ide/coqide/rocq_lex.mll b/ide/rocqide/rocq_lex.mll
similarity index 100%
rename from ide/coqide/rocq_lex.mll
rename to ide/rocqide/rocq_lex.mll
diff --git a/ide/coqide/rocqide.ml b/ide/rocqide/rocqide.ml
similarity index 97%
rename from ide/coqide/rocqide.ml
rename to ide/rocqide/rocqide.ml
index d416ff8072f7e..d3efb3f9ca3e1 100644
--- a/ide/coqide/rocqide.ml
+++ b/ide/rocqide/rocqide.ml
@@ -55,7 +55,7 @@ let logfile = ref None
 
 (** {2 Notebook of sessions } *)
 
-(** The main element of coqide is a notebook of session views *)
+(** The main element of rocqide is a notebook of session views *)
 
 let notebook =
   Wg_Notebook.create Session.build_layout Session.kill
@@ -113,7 +113,7 @@ let make_rocqtop_args fname =
       if List.exists (String.equal "-top") args then args
       else
         (* We basically copy the code of Names.check_valid since it is not exported *)
-        (* to coqide. This is to prevent a possible failure of parsing  "-topfile"  *)
+        (* to rocqide. This is to prevent a possible failure of parsing  "-topfile"  *)
         (* at initialization of rocqtop (see #10286) *)
         (* If the file name is a valid identifier, use it as toplevel name; *)
         (* otherwise the default “Top” will be used. *)
@@ -122,7 +122,7 @@ let make_rocqtop_args fname =
           | Some _ -> args
           | None -> "-topfile"::fname::args
         with Invalid_argument _ ->
-          failwith "CoqIDE cannot open files which do not have an extension in their filename."
+          failwith "RocqIDE cannot open files which do not have an extension in their filename."
   in
   proj, args
 
@@ -363,21 +363,21 @@ let close_and_quit () =
 
 (* Work around a deadlock due to OCaml exit cleanup. The standard [exit]
    function calls [flush_all], which can block if one of the opened channels is
-   not valid anymore. We do not register [at_exit] functions in CoqIDE, so
+   not valid anymore. We do not register [at_exit] functions in RocqIDE, so
    instead of flushing we simply die as gracefully as possible in the function
    below. *)
 external sys_exit : int -> 'a = "caml_sys_exit"
 
 let crash_save exitcode =
-  Minilib.log "Starting emergency save of buffers in .crashcoqide files";
+  Minilib.log "Starting emergency save of buffers in .crashrocqide files";
   let idx =
     let r = ref 0 in
     fun () -> incr r; string_of_int !r
   in
   let save_session sn =
     let filename = match sn.fileops#filename with
-      | None -> "Unnamed_coqscript_" ^ idx () ^ ".crashcoqide"
-      | Some f -> f^".crashcoqide"
+      | None -> "Unnamed_rocqscript_" ^ idx () ^ ".crashrocqide"
+      | Some f -> f^".crashrocqide"
     in
     try
       if try_export filename (sn.buffer#get_text ()) then
@@ -520,7 +520,7 @@ let print sn =
         Filename.quote (Filename.basename f_name) ^ " | " ^ cmd_print#get
       in
       let w = GWindow.window ~title:"Print" ~modal:true
-        ~position:`CENTER ~wmclass:("CoqIDE","CoqIDE") ()
+        ~position:`CENTER ~wmclass:("RocqIDE","RocqIDE") ()
       in
       let v = GPack.vbox ~spacing:10 ~border_width:10 ~packing:w#add ()
       in
@@ -572,7 +572,7 @@ let reset_autosave_timer () =
   if auto_save#get then
     FileOps.autosave_timer.run ~ms:auto_save_delay#get ~callback:autosave_all
 
-(** Export of functions used in [coqide_main] : *)
+(** Export of functions used in [rocqide_main] : *)
 
 let close_and_quit = FileAux.close_and_quit
 let crash_save = FileAux.crash_save
@@ -772,7 +772,7 @@ let resume_debugger ?sid opt =
       t.debugger#set_vars [];
       t.messages#default_route#set_editable2 false;
       t.messages#default_route#push Feedback.Notice (Pp.mt ());
-      (* Ideutils.push_info "Coq is computing";  todo: needs to be per-session *)
+      (* Ideutils.push_info "Rocq is computing";  todo: needs to be per-session *)
       true
     end else false
 
@@ -1000,7 +1000,7 @@ let log_file_message () =
 
 let initial_about () =
   let initial_string =
-    "Welcome to CoqIDE, an Integrated Development Environment for Coq"
+    "Welcome to RocqIDE, an Integrated Development Environment for Rocq"
   in
   let rocq_version = RocqDriver.short_version () in
   let version_info =
@@ -1159,7 +1159,7 @@ let about _ =
     with _ -> ()
   in
   let copyright =
-    "Coq is developed by the Coq Development Team\n\
+    "Rocq is developed by the Rocq Development Team\n\
      (INRIA - CNRS - LIX - LRI - PPS)"
   in
   let authors = [
@@ -1174,8 +1174,8 @@ let about _ =
     "Enrico Tassi";
     ]
   in
-  dialog#set_name "CoqIDE";
-  dialog#set_comments "The Coq Integrated Development Environment";
+  dialog#set_name "RocqIDE";
+  dialog#set_comments "The Rocq Integrated Development Environment";
   dialog#set_website Coq_config.wwwcoq;
   dialog#set_version Coq_config.version;
   dialog#set_copyright copyright;
@@ -1367,7 +1367,7 @@ let emit_to_focus window sgn =
   let obj = Gobject.unsafe_cast focussed_widget in
   try GtkSignal.emit_unit obj ~sgn with _ -> ()
 
-(** {2 Creation of the main coqide window } *)
+(** {2 Creation of the main rocqide window } *)
 
 let build_ui () =
   (* issue 12779 *)
@@ -1381,9 +1381,9 @@ let build_ui () =
     GtkData.StyleContext.ProviderPriority.application;
 
   let w = GWindow.window
-    ~wmclass:("CoqIDE","CoqIDE")
+    ~wmclass:("RocqIDE","RocqIDE")
     ~width:window_width#get ~height:window_height#get
-    ~title:"CoqIDE" ()
+    ~title:"RocqIDE" ()
   in
   let () =
     try w#set_icon (Some (GdkPixbuf.from_file (MiscMenu.rocq_icon ())))
@@ -1536,7 +1536,7 @@ let build_ui () =
     ("Forward", "_Forward", `GO_DOWN, Nav.forward_one, "Forward one command", "Down");
     ("Backward", "_Backward", `GO_UP, Nav.backward_one, "Backward one command", "Up");
     ("Run to cursor", "Run to _cursor", `JUMP_TO, Nav.run_to_cursor, "Run to cursor", "Right");
-    ("Reset", "_Reset", `GOTO_TOP, Nav.restart, "Reset Coq", "Home");
+    ("Reset", "_Reset", `GOTO_TOP, Nav.restart, "Reset Rocq", "Home");
     ("Run to end", "_Run to end", `GOTO_BOTTOM, Nav.run_to_end, "Run to end", "End");
     ("Fully check", "_Fully check", `EXECUTE, Nav.join_document, "Fully check the document", "Return");
     ("Interrupt", "_Interrupt", `STOP, Nav.interrupt, "Interrupt computations", "Break");
@@ -1655,17 +1655,17 @@ let build_ui () =
   w#add_accel_group Rocqide_ui.ui_m#get_accel_group ;
   GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
   if Config.gtk_platform <> `QUARTZ
-  then vbox#pack (Rocqide_ui.ui_m#get_widget "/CoqIDE MenuBar");
+  then vbox#pack (Rocqide_ui.ui_m#get_widget "/RocqIDE MenuBar");
 
   (* Connect some specific actions *)
-  let unicode = Rocqide_ui.ui_m#get_action "ui/CoqIDE MenuBar/Tools/LaTeX-to-unicode" in
+  let unicode = Rocqide_ui.ui_m#get_action "ui/RocqIDE MenuBar/Tools/LaTeX-to-unicode" in
   let callback b = unicode#set_sensitive b in
   let () = callback unicode_binding#get in
   let _ = unicode_binding#connect#changed ~callback in
 
   (* Toolbar *)
   let tbar = GtkButton.Toolbar.cast
-      ((Rocqide_ui.ui_m#get_widget "/CoqIDE ToolBar")#as_widget)
+      ((Rocqide_ui.ui_m#get_widget "/RocqIDE ToolBar")#as_widget)
   in
   let () = GtkButton.Toolbar.set
     ~orientation:`HORIZONTAL ~style:`ICONS tbar
@@ -1761,7 +1761,7 @@ let build_ui () =
   w
 
 
-(** {2 Coqide main function } *)
+(** {2 Rocqide main function } *)
 
 let make_file_buffer f =
   let f = if Filename.check_suffix f ".v" then f else f^".v" in
@@ -1787,24 +1787,24 @@ let main files =
 
 (** {2 Argument parsing } *)
 
-(** By default, the rocqtop we try to launch is exactly the current coqide
-    full name, with the last occurrence of "coqide" replaced by "coqtop".
+(** By default, the rocqtop we try to launch is exactly the current rocqide
+    full name, with the last occurrence of "rocqide" replaced by "coqtop".
     This should correctly handle the ".opt", ".byte", ".exe" situations.
     If the replacement fails, we default to "coqtop", hoping it's somewhere
-    in the path. Note that the -coqtop option to coqide overrides
+    in the path. Note that the -coqtop option to rocqide overrides
     this default coqtop path *)
 
 let rocqide_specific_usage = Boot.Usage.{
-  executable_name = "coqide";
+  executable_name = "rocqide";
   extra_args = "";
   extra_options = "\n\
-CoqIDE specific options:\
+RocqIDE specific options:\
 \n  -f _CoqProjectFile         set _CoqProject file to _CoqProjectFile\
 \n  -unicode-bindings f1 .. f2 load files f1..f2 with extra unicode bindings\
-\n  -coqtop dir                look for coqidetop in dir\
-\n  -coqtop-flags              extra flags for the coqtop subprocess\
+\n  -coqtop dir                look for rocqidetop in dir\
+\n  -coqtop-flags              extra flags for the rocqtop subprocess\
 \n  -debug                     enable debug mode\
-\n  -xml-debug                 enable debug mode and print XML messages to/from CoqIDE\
+\n  -xml-debug                 enable debug mode and print XML messages to/from RocqIDE\
 \n"
 }
 
@@ -1844,7 +1844,7 @@ let read_rocqide_args argv =
       filter_rocqtop rocqtop project_files bindings_files out args
     | ("-v" | "--version") :: _ ->
       (* This does the same thing as Usage.version () but printed differently *)
-      Printf.printf "CoqIDE, version %s\n" Coq_config.version;
+      Printf.printf "RocqIDE, version %s\n" Coq_config.version;
       (* Unlike rocqtop we don't accumulate queries so we exit immediately *)
       exit 0
     | ("-h"|"-H"|"-?"|"-help"|"--help") :: _ ->
diff --git a/ide/coqide/rocqide.mli b/ide/rocqide/rocqide.mli
similarity index 83%
rename from ide/coqide/rocqide.mli
rename to ide/rocqide/rocqide.mli
index 4e0787e43996b..3fbd3c73c0c17 100644
--- a/ide/coqide/rocqide.mli
+++ b/ide/rocqide/rocqide.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** * The CoqIDE main module *)
+(** * The RocqIDE main module *)
 
 (** The arguments that will be passed to rocqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
@@ -17,24 +17,24 @@ val sup_args : string list ref
 (** In debug mode under win32, messages are written to a log file *)
 val logfile : string option ref
 
-(** Filter the argv from coqide specific options, and set
+(** Filter the argv from rocqide specific options, and set
     Minilib.rocqtop_path accordingly *)
 val read_rocqide_args : string list -> string list
 
 (** Prepare the widgets, load the given files in tabs *)
 val main : string list -> GWindow.window
 
-(** Terminate coqide after closing all rocqtops and waiting
+(** Terminate rocqide after closing all rocqtops and waiting
     for their death *)
 val close_and_quit : unit -> unit
 
 (** Function to load of a file. *)
 val do_load : string -> unit
 
-(** Set coqide to perform a clean quit at Ctrl-C, while launching
+(** Set rocqide to perform a clean quit at Ctrl-C, while launching
     [crash_save] and exiting for others received signals *)
 val set_signal_handlers : ?parent:GWindow.window -> unit -> unit
 
-(** Emergency saving of opened files as "foo.v.crashcoqide",
+(** Emergency saving of opened files as "foo.v.crashrocqide",
     and exit (if the integer isn't 127). *)
 val crash_save : int -> unit
diff --git a/ide/coqide/rocqide_QUARTZ.c.in b/ide/rocqide/rocqide_QUARTZ.c.in
similarity index 100%
rename from ide/coqide/rocqide_QUARTZ.c.in
rename to ide/rocqide/rocqide_QUARTZ.c.in
diff --git a/ide/coqide/rocqide_QUARTZ.ml.in b/ide/rocqide/rocqide_QUARTZ.ml.in
similarity index 86%
rename from ide/coqide/rocqide_QUARTZ.ml.in
rename to ide/rocqide/rocqide_QUARTZ.ml.in
index 661d452125056..a8c54e79b65e0 100644
--- a/ide/coqide/rocqide_QUARTZ.ml.in
+++ b/ide/rocqide/rocqide_QUARTZ.ml.in
@@ -24,14 +24,14 @@ let () =
 let init () =
   let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication
     (GtkMenu.MenuShell.cast
-       (Rocqide_ui.ui_m#get_widget "/CoqIDE MenuBar")#as_widget)
+       (Rocqide_ui.ui_m#get_widget "/RocqIDE MenuBar")#as_widget)
   in
   let () = GtkosxApplication.Application.insert_app_menu_item
     osx#as_osxapplication
-    (Rocqide_ui.ui_m#get_widget "/CoqIDE MenuBar/Edit/Prefs")#as_widget 1
+    (Rocqide_ui.ui_m#get_widget "/RocqIDE MenuBar/Edit/Prefs")#as_widget 1
   in
   let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication
     (Some (GtkMenu.MenuItem.cast
-             (Rocqide_ui.ui_m#get_widget "/CoqIDE MenuBar/Help")#as_widget))
+             (Rocqide_ui.ui_m#get_widget "/RocqIDE MenuBar/Help")#as_widget))
   in
   osx#ready ()
diff --git a/ide/coqide/rocqide_WIN32.c.in b/ide/rocqide/rocqide_WIN32.c.in
similarity index 94%
rename from ide/coqide/rocqide_WIN32.c.in
rename to ide/rocqide/rocqide_WIN32.c.in
index 1ab7cac2743d5..4d6398d78cb23 100644
--- a/ide/coqide/rocqide_WIN32.c.in
+++ b/ide/rocqide/rocqide_WIN32.c.in
@@ -10,9 +10,9 @@
    prior code (f5276a11) is incorrect.  When it's present, it causes some of
    the strange behavior described in #13550.
    
-   This code signals all processes in the process group (multiple coqidetops) and coqide.
+   This code signals all processes in the process group (multiple coqidetops) and rocqide.
    because the console is shared. Rocqide.win_interrupt is used to ignore the signal sent
-   to CoqIDE. */
+   to RocqIDE. */
 
 CAMLprim value win32_interrupt(value pseudopid) {
   CAMLparam1(pseudopid);
diff --git a/ide/coqide/rocqide_WIN32.ml.in b/ide/rocqide/rocqide_WIN32.ml.in
similarity index 90%
rename from ide/coqide/rocqide_WIN32.ml.in
rename to ide/rocqide/rocqide_WIN32.ml.in
index f50062494a150..5e15ddbd015df 100644
--- a/ide/coqide/rocqide_WIN32.ml.in
+++ b/ide/rocqide/rocqide_WIN32.ml.in
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* On win32, we add the directory of coqide to the PATH at launch-time
+(* On win32, we add the directory of rocqide to the PATH at launch-time
    (this used to be done in a .bat script). *)
 
 let set_win32_path () =
@@ -16,7 +16,7 @@ let set_win32_path () =
     (Filename.dirname Sys.executable_name ^ ";" ^
       (try Sys.getenv "PATH" with _ -> ""))
 
-(* On win32, since coqide is now console-free, we re-route stdout/stderr
+(* On win32, since rocqide is now console-free, we re-route stdout/stderr
    to avoid Sys_error if someone writes to them. We write to a pipe which
    is never read (by default) or to a temp log file (when in debug mode).
 *)
@@ -27,7 +27,7 @@ let reroute_stdout_stderr () =
   Minilib.debug := debug;
   let out_descr =
     if debug then
-      let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
+      let (name,chan) = Filename.open_temp_file "rocqide_" ".log" in
       Rocqide.logfile := Some name;
       Unix.descr_of_out_channel chan
     else
diff --git a/ide/coqide/rocqide_X11.c.in b/ide/rocqide/rocqide_X11.c.in
similarity index 100%
rename from ide/coqide/rocqide_X11.c.in
rename to ide/rocqide/rocqide_X11.c.in
diff --git a/ide/coqide/rocqide_X11.ml.in b/ide/rocqide/rocqide_X11.ml.in
similarity index 100%
rename from ide/coqide/rocqide_X11.ml.in
rename to ide/rocqide/rocqide_X11.ml.in
diff --git a/ide/coqide/rocqide_main.ml b/ide/rocqide/rocqide_main.ml
similarity index 95%
rename from ide/coqide/rocqide_main.ml
rename to ide/rocqide/rocqide_main.ml
index 1f041c9f20901..66d8b11f0f78a 100644
--- a/ide/coqide/rocqide_main.ml
+++ b/ide/rocqide/rocqide_main.ml
@@ -29,7 +29,7 @@ let catch_gtk_messages () =
     else `INFO
   in
   let handler ~level msg =
-    let header = "CoqIDE internal error: " in
+    let header = "RocqIDE internal error: " in
     match log_level level with
       |`FATAL ->
         let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
@@ -68,5 +68,5 @@ let () =
     GMain.main ();
     failwith "Gtk loop ended"
   with e ->
-    Minilib.log ("CoqIDE unexpected error: " ^ Printexc.to_string e);
+    Minilib.log ("RocqIDE unexpected error: " ^ Printexc.to_string e);
     Rocqide.crash_save 127
diff --git a/ide/coqide/rocqide_main.mli b/ide/rocqide/rocqide_main.mli
similarity index 100%
rename from ide/coqide/rocqide_main.mli
rename to ide/rocqide/rocqide_main.mli
diff --git a/ide/coqide/rocqide_os_specific.mli b/ide/rocqide/rocqide_os_specific.mli
similarity index 100%
rename from ide/coqide/rocqide_os_specific.mli
rename to ide/rocqide/rocqide_os_specific.mli
diff --git a/ide/coqide/rocqide_ui.ml b/ide/rocqide/rocqide_ui.ml
similarity index 98%
rename from ide/coqide/rocqide_ui.ml
rename to ide/rocqide/rocqide_ui.ml
index 986bcad67f3ab..481d548a529b2 100644
--- a/ide/coqide/rocqide_ui.ml
+++ b/ide/rocqide/rocqide_ui.ml
@@ -29,7 +29,7 @@ let list_queries menu li =
 
 let init () =
   let theui = Printf.sprintf "<ui>\
-\n<menubar name='CoqIDE MenuBar'>\
+\n<menubar name='RocqIDE MenuBar'>\
 \n  <menu action='File'>\
 \n    <menuitem action='New' />\
 \n    <menuitem action='Open' />\
@@ -163,7 +163,7 @@ let init () =
 \n    <menuitem name='Abt' action='About Coq' />\
 \n  </menu>\
 \n</menubar>\
-\n<toolbar name='CoqIDE ToolBar'>\
+\n<toolbar name='RocqIDE ToolBar'>\
 \n  <toolitem action='Open' />\
 \n  <toolitem action='Save' />\
 \n  <toolitem action='Close buffer' />\
diff --git a/ide/coqide/rocqide_ui.mli b/ide/rocqide/rocqide_ui.mli
similarity index 100%
rename from ide/coqide/rocqide_ui.mli
rename to ide/rocqide/rocqide_ui.mli
diff --git a/ide/coqide/sentence.ml b/ide/rocqide/sentence.ml
similarity index 99%
rename from ide/coqide/sentence.ml
rename to ide/rocqide/sentence.ml
index a028d430bc075..62784d238d6dd 100644
--- a/ide/coqide/sentence.ml
+++ b/ide/rocqide/sentence.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** {1 Sentences in coqide buffers } *)
+(** {1 Sentences in rocqide buffers } *)
 
 (** Cut a part of the buffer in sentences and tag them.
     Invariant: either this slice ends the buffer, or it ends with ".".
diff --git a/ide/coqide/sentence.mli b/ide/rocqide/sentence.mli
similarity index 100%
rename from ide/coqide/sentence.mli
rename to ide/rocqide/sentence.mli
diff --git a/ide/coqide/session.ml b/ide/rocqide/session.ml
similarity index 100%
rename from ide/coqide/session.ml
rename to ide/rocqide/session.ml
diff --git a/ide/coqide/session.mli b/ide/rocqide/session.mli
similarity index 100%
rename from ide/coqide/session.mli
rename to ide/rocqide/session.mli
diff --git a/ide/coqide/shared.ml b/ide/rocqide/shared.ml
similarity index 93%
rename from ide/coqide/shared.ml
rename to ide/rocqide/shared.ml
index 72af404276ca3..fb4aaab5d2eee 100644
--- a/ide/coqide/shared.ml
+++ b/ide/rocqide/shared.ml
@@ -13,4 +13,4 @@ let cvt_pid = ref (fun pid -> pid)
 
 let get_interrupt_fname pid =
   Filename.concat (Filename.get_temp_dir_name ())
-      (Printf.sprintf "coqide_interrupt_%d" (!cvt_pid pid))
+      (Printf.sprintf "rocqide_interrupt_%d" (!cvt_pid pid))
diff --git a/ide/coqide/shared.mli b/ide/rocqide/shared.mli
similarity index 100%
rename from ide/coqide/shared.mli
rename to ide/rocqide/shared.mli
diff --git a/ide/coqide/shared_QUARTZ.c.in b/ide/rocqide/shared_QUARTZ.c.in
similarity index 100%
rename from ide/coqide/shared_QUARTZ.c.in
rename to ide/rocqide/shared_QUARTZ.c.in
diff --git a/ide/coqide/shared_QUARTZ.ml.in b/ide/rocqide/shared_QUARTZ.ml.in
similarity index 100%
rename from ide/coqide/shared_QUARTZ.ml.in
rename to ide/rocqide/shared_QUARTZ.ml.in
diff --git a/ide/coqide/shared_WIN32.c.in b/ide/rocqide/shared_WIN32.c.in
similarity index 100%
rename from ide/coqide/shared_WIN32.c.in
rename to ide/rocqide/shared_WIN32.c.in
diff --git a/ide/coqide/shared_WIN32.ml.in b/ide/rocqide/shared_WIN32.ml.in
similarity index 100%
rename from ide/coqide/shared_WIN32.ml.in
rename to ide/rocqide/shared_WIN32.ml.in
diff --git a/ide/coqide/shared_X11.c.in b/ide/rocqide/shared_X11.c.in
similarity index 100%
rename from ide/coqide/shared_X11.c.in
rename to ide/rocqide/shared_X11.c.in
diff --git a/ide/coqide/shared_X11.ml.in b/ide/rocqide/shared_X11.ml.in
similarity index 100%
rename from ide/coqide/shared_X11.ml.in
rename to ide/rocqide/shared_X11.ml.in
diff --git a/ide/coqide/shared_os_specific.mli b/ide/rocqide/shared_os_specific.mli
similarity index 100%
rename from ide/coqide/shared_os_specific.mli
rename to ide/rocqide/shared_os_specific.mli
diff --git a/ide/coqide/tags.ml b/ide/rocqide/tags.ml
similarity index 100%
rename from ide/coqide/tags.ml
rename to ide/rocqide/tags.ml
diff --git a/ide/coqide/tags.mli b/ide/rocqide/tags.mli
similarity index 100%
rename from ide/coqide/tags.mli
rename to ide/rocqide/tags.mli
diff --git a/ide/coqide/ui_dialogs.ml b/ide/rocqide/ui_dialogs.ml
similarity index 100%
rename from ide/coqide/ui_dialogs.ml
rename to ide/rocqide/ui_dialogs.ml
diff --git a/ide/coqide/ui_dialogs.mli b/ide/rocqide/ui_dialogs.mli
similarity index 100%
rename from ide/coqide/ui_dialogs.mli
rename to ide/rocqide/ui_dialogs.mli
diff --git a/ide/coqide/unicode_bindings.ml b/ide/rocqide/unicode_bindings.ml
similarity index 100%
rename from ide/coqide/unicode_bindings.ml
rename to ide/rocqide/unicode_bindings.ml
diff --git a/ide/coqide/unicode_bindings.mli b/ide/rocqide/unicode_bindings.mli
similarity index 100%
rename from ide/coqide/unicode_bindings.mli
rename to ide/rocqide/unicode_bindings.mli
diff --git a/ide/coqide/utf8_convert.mli b/ide/rocqide/utf8_convert.mli
similarity index 100%
rename from ide/coqide/utf8_convert.mli
rename to ide/rocqide/utf8_convert.mli
diff --git a/ide/coqide/utf8_convert.mll b/ide/rocqide/utf8_convert.mll
similarity index 73%
rename from ide/coqide/utf8_convert.mll
rename to ide/rocqide/utf8_convert.mll
index d9da8f579b536..e3f79df544386 100644
--- a/ide/coqide/utf8_convert.mll
+++ b/ide/rocqide/utf8_convert.mll
@@ -23,23 +23,23 @@ let long = short short
 rule entry = parse
   | "\\x{" (short | long ) '}'
       { let s = lexeme lexbuf in
-	let n = String.length s in
-	let code =
-	  try Glib.Utf8.from_unichar
-	    (int_of_string ("0x"^(String.sub s 3 (n - 4))))
-	  with _ -> s
-	in
-	let c = if Glib.Utf8.validate code then code else s in
-	Buffer.add_string b c;
-	entry lexbuf
+        let n = String.length s in
+        let code =
+          try Glib.Utf8.from_unichar
+            (int_of_string ("0x"^(String.sub s 3 (n - 4))))
+          with _ -> s
+        in
+        let c = if Glib.Utf8.validate code then code else s in
+        Buffer.add_string b c;
+        entry lexbuf
       }
   | _
       { let s = lexeme lexbuf in
-	Buffer.add_string b s;
-	entry lexbuf}
+        Buffer.add_string b s;
+        entry lexbuf}
   | eof
       {
-	let s = Buffer.contents b in Buffer.reset b ; s
+        let s = Buffer.contents b in Buffer.reset b ; s
       }
 
 
diff --git a/ide/coqide/wg_Command.ml b/ide/rocqide/wg_Command.ml
similarity index 100%
rename from ide/coqide/wg_Command.ml
rename to ide/rocqide/wg_Command.ml
diff --git a/ide/coqide/wg_Command.mli b/ide/rocqide/wg_Command.mli
similarity index 100%
rename from ide/coqide/wg_Command.mli
rename to ide/rocqide/wg_Command.mli
diff --git a/ide/coqide/wg_Completion.ml b/ide/rocqide/wg_Completion.ml
similarity index 100%
rename from ide/coqide/wg_Completion.ml
rename to ide/rocqide/wg_Completion.ml
diff --git a/ide/coqide/wg_Completion.mli b/ide/rocqide/wg_Completion.mli
similarity index 100%
rename from ide/coqide/wg_Completion.mli
rename to ide/rocqide/wg_Completion.mli
diff --git a/ide/coqide/wg_Debugger.ml b/ide/rocqide/wg_Debugger.ml
similarity index 100%
rename from ide/coqide/wg_Debugger.ml
rename to ide/rocqide/wg_Debugger.ml
diff --git a/ide/coqide/wg_Debugger.mli b/ide/rocqide/wg_Debugger.mli
similarity index 100%
rename from ide/coqide/wg_Debugger.mli
rename to ide/rocqide/wg_Debugger.mli
diff --git a/ide/coqide/wg_Detachable.ml b/ide/rocqide/wg_Detachable.ml
similarity index 99%
rename from ide/coqide/wg_Detachable.ml
rename to ide/rocqide/wg_Detachable.ml
index 53a83d7f52632..0e957bbf4c33e 100644
--- a/ide/coqide/wg_Detachable.ml
+++ b/ide/rocqide/wg_Detachable.ml
@@ -98,4 +98,3 @@ let detachable ?title =
          let d = new detachable (GtkPack.Box.create `HORIZONTAL p) in
          Option.iter d#set_title title;
          d))
-
diff --git a/ide/coqide/wg_Detachable.mli b/ide/rocqide/wg_Detachable.mli
similarity index 99%
rename from ide/coqide/wg_Detachable.mli
rename to ide/rocqide/wg_Detachable.mli
index 2b71044e8cf76..6cc6855b78e65 100644
--- a/ide/coqide/wg_Detachable.mli
+++ b/ide/rocqide/wg_Detachable.mli
@@ -42,5 +42,3 @@ val detachable :
   ?width:int ->
   ?height:int ->
   ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> detachable
-
-
diff --git a/ide/coqide/wg_Find.ml b/ide/rocqide/wg_Find.ml
similarity index 100%
rename from ide/coqide/wg_Find.ml
rename to ide/rocqide/wg_Find.ml
diff --git a/ide/coqide/wg_Find.mli b/ide/rocqide/wg_Find.mli
similarity index 100%
rename from ide/coqide/wg_Find.mli
rename to ide/rocqide/wg_Find.mli
diff --git a/ide/coqide/wg_MessageView.ml b/ide/rocqide/wg_MessageView.ml
similarity index 100%
rename from ide/coqide/wg_MessageView.ml
rename to ide/rocqide/wg_MessageView.ml
diff --git a/ide/coqide/wg_MessageView.mli b/ide/rocqide/wg_MessageView.mli
similarity index 100%
rename from ide/coqide/wg_MessageView.mli
rename to ide/rocqide/wg_MessageView.mli
diff --git a/ide/coqide/wg_Notebook.ml b/ide/rocqide/wg_Notebook.ml
similarity index 99%
rename from ide/coqide/wg_Notebook.ml
rename to ide/rocqide/wg_Notebook.ml
index 6b1aa091b9252..164aaf9135ca0 100644
--- a/ide/coqide/wg_Notebook.ml
+++ b/ide/rocqide/wg_Notebook.ml
@@ -73,4 +73,3 @@ let create make kill =
              ~create:(fun pl ->
                         let nb = GtkPack.Notebook.create pl in
                          (new typed_notebook make kill nb)))
-
diff --git a/ide/coqide/wg_Notebook.mli b/ide/rocqide/wg_Notebook.mli
similarity index 100%
rename from ide/coqide/wg_Notebook.mli
rename to ide/rocqide/wg_Notebook.mli
diff --git a/ide/coqide/wg_ProofView.ml b/ide/rocqide/wg_ProofView.ml
similarity index 100%
rename from ide/coqide/wg_ProofView.ml
rename to ide/rocqide/wg_ProofView.ml
diff --git a/ide/coqide/wg_ProofView.mli b/ide/rocqide/wg_ProofView.mli
similarity index 100%
rename from ide/coqide/wg_ProofView.mli
rename to ide/rocqide/wg_ProofView.mli
diff --git a/ide/coqide/wg_RoutedMessageViews.ml b/ide/rocqide/wg_RoutedMessageViews.ml
similarity index 100%
rename from ide/coqide/wg_RoutedMessageViews.ml
rename to ide/rocqide/wg_RoutedMessageViews.ml
diff --git a/ide/coqide/wg_RoutedMessageViews.mli b/ide/rocqide/wg_RoutedMessageViews.mli
similarity index 100%
rename from ide/coqide/wg_RoutedMessageViews.mli
rename to ide/rocqide/wg_RoutedMessageViews.mli
diff --git a/ide/coqide/wg_ScriptView.ml b/ide/rocqide/wg_ScriptView.ml
similarity index 100%
rename from ide/coqide/wg_ScriptView.ml
rename to ide/rocqide/wg_ScriptView.ml
diff --git a/ide/coqide/wg_ScriptView.mli b/ide/rocqide/wg_ScriptView.mli
similarity index 100%
rename from ide/coqide/wg_ScriptView.mli
rename to ide/rocqide/wg_ScriptView.mli
diff --git a/ide/coqide/wg_Segment.ml b/ide/rocqide/wg_Segment.ml
similarity index 100%
rename from ide/coqide/wg_Segment.ml
rename to ide/rocqide/wg_Segment.ml
diff --git a/ide/coqide/wg_Segment.mli b/ide/rocqide/wg_Segment.mli
similarity index 100%
rename from ide/coqide/wg_Segment.mli
rename to ide/rocqide/wg_Segment.mli
diff --git a/man/dune b/man/dune
index 3703c2fc2ccfe..3ce1ca6370b74 100644
--- a/man/dune
+++ b/man/dune
@@ -10,6 +10,5 @@
 
 (install
  (section man)
- (package coqide)
- (files coqide.1))
-
+ (package rocqide)
+ (files rocqide.1))
diff --git a/man/coqide.1 b/man/rocqide.1
similarity index 68%
rename from man/coqide.1
rename to man/rocqide.1
index 504b52c254dc4..34b0454ca6e24 100644
--- a/man/coqide.1
+++ b/man/rocqide.1
@@ -1,24 +1,22 @@
-.TH COQIDE 1
+.TH ROCQIDE 1
 .
 .SH NAME
-coqide \- graphical interface for the Coq proof assistant
+rocqide \- graphical interface for the Rocq proof assistant
 .
 .
 .SH SYNOPSIS
-.B coqide
+.B rocqide
 [
 options
 ]
 .
 .SH DESCRIPTION
 .
-.B coqide
-is a gtk graphical interface for the Coq proof assistant.
+.B rocqide
+is a gtk graphical interface for the Rocq proof assistant.
 .PP
-For command-line-oriented use of Coq, see
-.BR coqtop (1);
-for batch-oriented use of Coq, see
-.BR coqc (1).
+For command-line-oriented or batch-oriented use of Rocq, see
+.BR rocq (1);
 .
 .
 .SH OPTIONS
@@ -26,18 +24,18 @@ for batch-oriented use of Coq, see
 .TP
 .B \-h
 Show the complete list of options accepted by
-.BR coqide .
+.BR rocqide .
 .TP
 .BI \-I\  dir, \ \-include\  dir
 Add directory
 .I dir
 in the include path.
 .TP
-.BI \-R\  dir\ coqdir
+.BI \-R\  dir\ rocqdir
 Recursively map physical
 .I dir
 to logical
-.I coqdir.
+.I rocqdir.
 .TP
 .B \-src
 Add source directories in the include path.
@@ -54,46 +52,46 @@ Load ML file
 .I f.
 .TP
 .BI \-l\  f, \ \-load\-vernac\-source\  f
-Load Coq file
+Load Rocq file
 .IR f .v
 (Load
 .IR f. ).
 .TP
 .BI \-lv\  f, \ \-load\-vernac\-source\-verbose\  f
-Load Coq file
+Load Rocq file
 .IR f .v
 (Load Verbose
 .IR f. ).
 .TP
 .BI \-load\-vernac\-object\  path
-Load Coq library
+Load Rocq library
 .I path
 (Require
 .IR path. ).
 .TP
 .BI \-require-import\  path
-Load Coq library
+Load Rocq library
 .I path
 and import it (Require Import
 .IR path. ).
 .TP
 .BI \-compile\  f
-Compile Coq file
+Compile Rocq file
 .IR f .v
 (implies
 .BR \-batch ).
 .TP
 .BI \-compile\-verbose\  f
-Verbosely compile Coq file
+Verbosely compile Rocq file
 .IR f .v
 (implies
 .BR -batch ).
 .TP
 .B \-where
-Print Coq's standard library location and exit.
+Print Rocq's standard library location and exit.
 .TP
 .B -v
-Print Coq version and exit.
+Print Rocq version and exit.
 .TP
 .B \-q
 Skip loading of rcfile.
@@ -103,13 +101,13 @@ Set the rcfile to
 .I f.
 .TP
 .B \-emacs
-Tells Coq it is executed under Emacs.
+Tells Rocq it is executed under Emacs.
 .TP
 .BI \-dump\-glob\  f
 Dump globalizations in file
 .I f
 (to be used by
-.BR coqdoc (1)).
+.BR rocq (1) doc).
 .TP
 .B \-impredicative\-set
 Set sort Set impredicative.
@@ -119,17 +117,14 @@ Don't load opaque proofs in memory.
 .
 .SH SEE ALSO
 .
-.BR coqc (1),
-.BR coqtop (1),
-.BR coq\-tex (1),
-.BR coqdep (1)
+.BR rocq (1),
 .PP
 .I
-The Coq Reference Manual
+The Rocq Reference Manual
 .PP
 The Coq web site: http://coq.inria.fr
 .PP
-/usr/share/doc/coqide/FAQ
+/usr/share/doc/rocqide/FAQ
 .
 .SH AUTHOR
 This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 596fe42661fc9..6ab7b44f3e36c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -493,7 +493,7 @@ let print_one_decl struc mp decl =
 (*s Extraction of a ml struct to a file. *)
 
 (** For Recursive Extraction, writing directly on stdout
-    won't work with coqide, we use a buffer instead *)
+    won't work with rocqide, we use a buffer instead *)
 
 let buf = Buffer.create 1000
 
@@ -573,7 +573,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
        end;
        info_file si)
     (if dry then None else si);
-  (* Print the buffer content via Rocq standard formatter (ok with coqide). *)
+  (* Print the buffer content via Rocq standard formatter (ok with rocqide). *)
   if not (Int.equal (Buffer.length buf) 0) then begin
     Feedback.msg_notice (str (Buffer.contents buf));
     Buffer.reset buf
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 87bbb94abf75b..78c103da647b6 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (*
-Displays the differences between successive proof steps in coqtop and CoqIDE.
+Displays the differences between successive proof steps in coqtop and RocqIDE.
 Proof General requires minor changes to make the diffs visible, but this code
 shouldn't break the existing version of PG.  See pp_diff.ml for details on how
 the diff works.
@@ -18,12 +18,12 @@ Diffs are computed for the hypotheses and conclusion of each goal in the new
 proof with its matching goal in the old proof.
 
 Diffs can be enabled in coqtop with 'Set Diffs "on"|"off"|"removed"' or
-'-diffs on|off|removed' on the OS command line.  In CoqIDE, they can be enabled
+'-diffs on|off|removed' on the OS command line.  In RocqIDE, they can be enabled
 from the View menu.  The "on" option shows only the new item with added text,
 while "removed" shows each modified item twice--once with the old value showing
 removed text and once with the new value showing added text.
 
-In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
+In RocqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
 For coqtop, these can be set through the ROCQ_COLORS environment variable.
 
 Limitations/Possible enhancements:
@@ -33,7 +33,7 @@ not the greatest.  I didn't want to change the existing green highlight.
 Suggestions welcome.
 
 - coqtop underlines removed text because (per Wikipedia) the ANSI escape code
-for strikeout is not commonly supported (it didn't work on my system).  CoqIDE
+for strikeout is not commonly supported (it didn't work on my system).  RocqIDE
 uses strikeout on removed text.
 *)
 
diff --git a/coqide.opam b/rocqide.opam
similarity index 94%
rename from coqide.opam
rename to rocqide.opam
index d9ea193f88105..66487d157f25c 100644
--- a/coqide.opam
+++ b/rocqide.opam
@@ -8,7 +8,7 @@ a formal language to write mathematical definitions, executable
 algorithms and theorems together with an environment for
 semi-interactive development of machine-checked proofs.
 
-This package provides the CoqIDE, a graphical user interface for the
+This package provides the RocqIDE, a graphical user interface for the
 development of interactive proofs."""
 maintainer: ["The Coq development team <coqdev@inria.fr>"]
 authors: ["The Coq development team, INRIA, CNRS, and contributors"]
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index cffc836d5f296..3aa5a3dee9d2d 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -109,7 +109,7 @@ module type Task = sig
 
       These functions are meant to parametrize the worker manager on
       the actions to be taken when things go wrong or are cancelled
-      (you can kill a worker in CoqIDE, or using kill -9...)
+      (you can kill a worker in RocqIDE, or using kill -9...)
 
       E.g. master can decide to inhabit the (delegate) Future.t with a
       closure (to be run in master), i.e. make the document still
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
index 7516c47e1ef87..6028bbc096e2c 100644
--- a/test-suite/ide/blocking-futures.fake
+++ b/test-suite/ide/blocking-futures.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Extraction will force the future computation, assert it is blocking
diff --git a/test-suite/ide/fake_ide.ml b/test-suite/ide/fake_ide.ml
index b4fc785f94a1f..dc17a4a49d694 100644
--- a/test-suite/ide/fake_ide.ml
+++ b/test-suite/ide/fake_ide.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Fake_ide : Simulate a [coqide] talking to a [coqidetop]. *)
+(** Fake_ide : Simulate a [rocqide] talking to a [coqidetop]. *)
 
 let error s =
   prerr_endline ("fake_ide: error: "^s);
@@ -308,7 +308,7 @@ let usage () =
     (Parser.print grammar));
   exit 1
 
-module Coqide = Spawn.Sync ()
+module Rocqide = Spawn.Sync ()
 
 let main =
   if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
@@ -326,7 +326,7 @@ let main =
   prerr_endline ("Running: "^idetop_name^" "^
                    (String.concat " " (Array.to_list coqtop_args)));
   let coq =
-    let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in
+    let _p, cin, cout = Rocqide.spawn idetop_name coqtop_args in
     let ip = Xml_parser.make (Xml_parser.SChannel cin) in
     let op = Xml_printer.make (Xml_printer.TChannel cout) in
     Xml_parser.check_eof ip false;
diff --git a/test-suite/ide/join-idem.fake b/test-suite/ide/join-idem.fake
index c24c55b7a047b..ffffe0115516e 100644
--- a/test-suite/ide/join-idem.fake
+++ b/test-suite/ide/join-idem.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Idempotency of join
diff --git a/test-suite/ide/join-module1.fake b/test-suite/ide/join-module1.fake
index d313210986fa0..f4c1b44507dd3 100644
--- a/test-suite/ide/join-module1.fake
+++ b/test-suite/ide/join-module1.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Join from within a module.
diff --git a/test-suite/ide/join-module2.fake b/test-suite/ide/join-module2.fake
index 3c19ecb184cb6..71b15de0bc0c8 100644
--- a/test-suite/ide/join-module2.fake
+++ b/test-suite/ide/join-module2.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Failing join from within a module
diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake
index 236028ce46e3d..4f492a1ead9b6 100644
--- a/test-suite/ide/join-sync.fake
+++ b/test-suite/ide/join-sync.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Error resiliency + async proofs off
diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake
index c4c696ad9a181..69e4f1b666d91 100644
--- a/test-suite/ide/join.fake
+++ b/test-suite/ide/join.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Error resiliency
diff --git a/test-suite/ide/reopen.fake b/test-suite/ide/reopen.fake
index 8166d0137e2be..6a1a38551f253 100644
--- a/test-suite/ide/reopen.fake
+++ b/test-suite/ide/reopen.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # jumping between broken proofs + interp error while fixing.
diff --git a/test-suite/ide/reopen1.fake b/test-suite/ide/reopen1.fake
index 2c4f13de86283..b0618c770ad75 100644
--- a/test-suite/ide/reopen1.fake
+++ b/test-suite/ide/reopen1.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # jumping outside the focused zone should signal an unfocus.
diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
index 552636157accf..91fda4bd60232 100644
--- a/test-suite/ide/undo001.fake
+++ b/test-suite/ide/undo001.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Simple backtrack by 1 between two global definitions
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index eb553f9dfa7e2..2a5ba893d3c51 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Simple backtrack by 2 before two global definitions
diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake
index 90757627662ea..c1de67a0ce18d 100644
--- a/test-suite/ide/undo003.fake
+++ b/test-suite/ide/undo003.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Simple backtrack by 0 should be a no-op
diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake
index 9029b03e24666..4284708dd70f9 100644
--- a/test-suite/ide/undo004.fake
+++ b/test-suite/ide/undo004.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Undoing arbitrary commands, as first step
diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake
index 7e31c0b05f2f5..fe1bb691e4f6c 100644
--- a/test-suite/ide/undo005.fake
+++ b/test-suite/ide/undo005.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Undoing arbitrary commands, as non-first step
diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake
index cdfdee1b7a60b..f9979642c318e 100644
--- a/test-suite/ide/undo006.fake
+++ b/test-suite/ide/undo006.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Undoing declarations, as first step
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
index 72cab7a30e247..db108c9c316ba 100644
--- a/test-suite/ide/undo008.fake
+++ b/test-suite/ide/undo008.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Undoing declarations, as non-first step
diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
index 76f400ef06b09..13968b11a2d5d 100644
--- a/test-suite/ide/undo009.fake
+++ b/test-suite/ide/undo009.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Undoing declarations, interleaved with proof steps
diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake
index 524416c32b664..b69dc007fb470 100644
--- a/test-suite/ide/undo010.fake
+++ b/test-suite/ide/undo010.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Undoing declarations, interleaved with proof steps and commands *)
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
index c95df1b11c941..2d126397d5d2e 100644
--- a/test-suite/ide/undo012.fake
+++ b/test-suite/ide/undo012.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index a3ccefd2ca002..a41c17faa7791 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
index 13e718229c986..b6cea420ea30c 100644
--- a/test-suite/ide/undo014.fake
+++ b/test-suite/ide/undo014.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
index 9cbd64460dda2..ba62d72ff5af9 100644
--- a/test-suite/ide/undo015.fake
+++ b/test-suite/ide/undo015.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index 15bd3cc92d616..03148323941fd 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake
index 37423dc72773a..459c010952087 100644
--- a/test-suite/ide/undo017.fake
+++ b/test-suite/ide/undo017.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # bug #2569 : Undoing inside modules
diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake
index 11091bfa67cdc..68d23ff62061c 100644
--- a/test-suite/ide/undo018.fake
+++ b/test-suite/ide/undo018.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # bug #2569 : Undoing inside section
diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake
index 5df49ebbb75a7..6eb7eafe7c53b 100644
--- a/test-suite/ide/undo019.fake
+++ b/test-suite/ide/undo019.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # bug #2569 : Undoing a focused subproof
diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake
index aa1d9bb2a72a2..bff7cf7ae50e1 100644
--- a/test-suite/ide/undo020.fake
+++ b/test-suite/ide/undo020.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # focusing a broken proof and fixing it
diff --git a/test-suite/ide/undo021.fake b/test-suite/ide/undo021.fake
index 0d83ad25ac16a..f70167c2c2998 100644
--- a/test-suite/ide/undo021.fake
+++ b/test-suite/ide/undo021.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # jumping between broken proofs
diff --git a/test-suite/ide/undo022.fake b/test-suite/ide/undo022.fake
index 51d8d106e34fe..cf9396bdafc71 100644
--- a/test-suite/ide/undo022.fake
+++ b/test-suite/ide/undo022.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # jumping between broken proofs + interp error while fixing.
diff --git a/test-suite/ide/univ.fake b/test-suite/ide/univ.fake
index 90af8785ad2bb..dd2d0901b3bc8 100644
--- a/test-suite/ide/univ.fake
+++ b/test-suite/ide/univ.fake
@@ -1,4 +1,4 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
+# Script simulating a dialog between rocqide and coqtop -ideslave
 # Run it via fake_ide
 #
 # jumping between broken proofs + interp error while fixing.
diff --git a/test-suite/success/RemoteUnivs.v b/test-suite/success/RemoteUnivs.v
index 5ab4937ddabd4..3bf2ccabe61c2 100644
--- a/test-suite/success/RemoteUnivs.v
+++ b/test-suite/success/RemoteUnivs.v
@@ -11,7 +11,7 @@ Proof.
   exact Type.
 Qed.
 
-(* (* coqide test, note the delegated proofs seem to get an empty dirpath?
+(* (* rocqide test, note the delegated proofs seem to get an empty dirpath?
       or I got confused because I had lemma foo in file foo
  *)
 Definition U := Type.
diff --git a/tools/configure/cmdArgs.mli b/tools/configure/cmdArgs.mli
index d284819a1df20..f5aeaf4ab1b3c 100644
--- a/tools/configure/cmdArgs.mli
+++ b/tools/configure/cmdArgs.mli
@@ -33,7 +33,7 @@ type t =
   ; natdynlink : bool
   (** native dynlink enabled [only relevant to coq_makefile] *)
   ; browser : string option
-  (** override default browser command [for CoqIDE] *)
+  (** override default browser command [for RocqIDE] *)
   ; bytecodecompiler : bool
   (** Enable/disable Coq's VM *)
   ; nativecompiler : nativecompiler
diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml
index 2b04857f7ab59..5c8833ac13844 100644
--- a/tools/configure/configure.ml
+++ b/tools/configure/configure.ml
@@ -229,8 +229,8 @@ end
 let install prefs =
   [ InstallDir.make "COQPREFIX" "Corelib" prefs.prefix (Relative "") (Relative "")
   ; InstallDir.make "COQLIBINSTALL" "the Coq library" prefs.libdir (Relative "lib/coq") (Relative "lib/coq")
-  ; InstallDir.make "CONFIGDIR" "the Coqide configuration files" prefs.configdir (Relative "config") (Absolute "/etc/xdg/coq")
-  ; InstallDir.make "DATADIR" "the Coqide data files" prefs.datadir (Relative "share/coq") (Relative "share/coq")
+  ; InstallDir.make "CONFIGDIR" "the Rocqide configuration files" prefs.configdir (Relative "config") (Absolute "/etc/xdg/coq")
+  ; InstallDir.make "DATADIR" "the Rocqide data files" prefs.datadir (Relative "share/coq") (Relative "share/coq")
   ; InstallDir.make "MANDIR" "the Coq man pages" prefs.mandir (Relative "share/man") (Relative "share/man")
   ; InstallDir.make "DOCDIR" "documentation prefix path for all Coq packages" prefs.docdir (Relative "share/doc") (Relative "share/doc")
   ]
diff --git a/tools/configure/util.ml b/tools/configure/util.ml
index fe797c6b0f08b..c56b92e65fe49 100644
--- a/tools/configure/util.ml
+++ b/tools/configure/util.ml
@@ -70,7 +70,6 @@ let read_lines_and_close_fd fd =
 (** Run some unix command and read the first line of its output.
     We avoid Unix.open_process and its non-fully-portable /bin/sh,
     especially when it comes to quoting the filenames.
-    See open_process_pid in ide/coqide/coq.ml for more details.
     Error messages:
      - if err=StdErr, any error message goes in the stderr of our script.
      - if err=StdOut, we merge stderr and stdout (just as 2>&1).
diff --git a/vernac/future.ml b/vernac/future.ml
index c7c5321f2818d..02add790988c1 100644
--- a/vernac/future.ml
+++ b/vernac/future.ml
@@ -11,13 +11,13 @@
 let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
-                "the \"-async-proofs off\" option to CoqIDE to disable "^
+                "the \"-async-proofs off\" option to Rocqide to disable "^
                 "asynchronous script processing and don't pass \"-vio\" to "^
                 "coqc."))
 let not_here_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
-                "the \"-async-proofs off\" option to CoqIDE to disable "^
+                "the \"-async-proofs off\" option to Rocqide to disable "^
                 "asynchronous script processing and don't pass \"-vio\" to "^
                 "coqc."))