Merge PR #8636: [doc] [api] Remove `ocamldoc` support in favor of `odoc`

6 files changed, 3 insertions, 296 deletions

diff --git a/dev/README.md b/dev/README.md
index 4642aaf06d..d9fdd230d3 100644
--- a/dev/README.md
+++ b/dev/README.md
@@ -34,9 +34,8 @@
 | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release |
 
 
-## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`)
-`make mli-doc` in coq root directory.
-
+## Documentation of ML interfaces using `odoc` ( `_build/default/_doc`)
+`make -f Makefile.dune apidoc` in coq root directory.
 
 ## Other development tools (`dev/tools`)
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 3a179a9431..24952eb5b7 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -167,10 +167,7 @@ Currently available artifacts are:
   + Coq's Standard Library Documentation [master branch]
     https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman
   + Coq's ML API Documentation [master branch]
-    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc
-
-  The dune job also provides its own API documentation using the newer `odoc` tool:
-  https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
 
 ### GitLab and Windows
 
diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro
deleted file mode 100644
index 33d20fc818..0000000000
--- a/dev/ocamldoc/docintro
+++ /dev/null
@@ -1,49 +0,0 @@
-{!indexlist}
-
-This is Coq, a proof assistant for the Calculus of Inductive Constructions.
-This document describes the implementation of Coq.
-It has been automatically generated from the source of
-Coq using {{:http://caml.inria.fr/}ocamldoc}.
-The source files are organized in several directories ordered like that:
-
-{ol {- Utility libraries : lib
-
-describes the various utility libraries used in the code
-of Coq.}
-{- Kernel : kernel
-
-describes the Coq kernel, which is a type checker for the Calculus
-of Inductive Constructions.}
-{- Library : library
-
-describes the Coq library, which is made of two parts:
-- a general mechanism to keep a trace of all operations and of
-    the state of the system, with backtrack capabilities;
-- a global environment for the CCI, with functions to export and 
-    import compiled modules.
-
-}
-{- Pretyping : pretyping
-
-}
-{- Front abstract syntax of terms : interp
-
-describes the translation from Coq context-dependent
-front abstract syntax of terms {v constr_expr v} to and from the
-context-free, untyped, globalized form of constructions {v glob_constr v}.}
-{- Parsers and printers : parsing
-
-describes the implementation of the Coq parsers and printers.}
-{- Proof engine : proofs
-
-describes the Coq proof engine, which is also called
-the ``refiner'', since it provides a way to build terms by successive
-refining steps. Those steps are either primitive rules or higher-level
-tactics.}
-{- Tacticts : tactics
-
-describes the Coq main tactics.}
-{- Toplevel : toplevel
-
-describes the highest modules of the Coq system.}
-}
diff --git a/dev/ocamldoc/fix-ocamldoc-utf8 b/dev/ocamldoc/fix-ocamldoc-utf8
deleted file mode 100755
index fe2e0c1155..0000000000
--- a/dev/ocamldoc/fix-ocamldoc-utf8
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-# This reverts automatic translation of latin1 accentuated letters by ocamldoc
-# Usage: fix-ocamldoc-utf8 file
-
-sed -i -e 's/\\`a/\d224/g' -e "s/\\\^a/\d226/g" -e "s/\\\'e/\d233/g" -e 's/\\`e/\d232/g' -e "s/\\\^e/\d234/g" -e 's/\\\"e/\d235/g' -e "s/\\\^o/\d244/g" -e 's/\\\"o/\d246/g' -e "s/\\\^i/\d238/g" -e 's/\\\"i/\d239/g' -e 's/\\`u/\d249/g' -e "s/\\\^u/\d251/g" -e "s/\\\c{c}/\d231/g" $1
diff --git a/dev/ocamldoc/header.tex b/dev/ocamldoc/header.tex
deleted file mode 100644
index 4091f8144f..0000000000
--- a/dev/ocamldoc/header.tex
+++ /dev/null
@@ -1,14 +0,0 @@
-\documentclass[11pt]{article} 
-\usepackage[utf8x]{inputenc} 
-\usepackage[T1]{fontenc} 
-\usepackage{textcomp}
-\usepackage{tipa}
-\usepackage{textgreek}
-\usepackage{fullpage} 
-\usepackage{url} 
-\usepackage{ocamldoc}
-\title{Coq mlis documentation}
-\begin{document}
-\maketitle
-\tableofcontents
-\vspace{0.2cm}
diff --git a/dev/ocamldoc/html/style.css b/dev/ocamldoc/html/style.css
deleted file mode 100644
index c2c45b6297..0000000000
--- a/dev/ocamldoc/html/style.css
+++ /dev/null
@@ -1,220 +0,0 @@
-a:visited {

-  color: #416DFF; text-decoration: none; 

-}

-

-a:link {

-  color: #416DFF; text-decoration: none;

-}

-

-a:hover {

-  color: Red; text-decoration: none; background-color: #5FFF88

-}

-

-a:active {

-  color: Red; text-decoration: underline; 

-}

-

-.keyword {

-  font-weight: bold; color: Red 

-}

-

-.keywordsign {

-  color: #C04600 

-}

-

-.superscript {

-  font-size: 8 

-}

-

-.subscript {

-  font-size: 8 

-}

-

-.comment {

-  color: Green 

-}

-

-.constructor {

-  color: Blue 

-}

-

-.type {

-  color: #5C6585 

-}

-

-.string {

-  color: Maroon 

-}

-

-.warning {

-  color: Red; font-weight: bold 

-}

-

-.info {

-  margin-left: 3em; margin-right: 3em 

-}

-

-.param_info {

-  margin-top: 4px; margin-left: 3em; margin-right: 3em 

-}

-

-.code {

-  color: #465F91; 

-}

-

-h1 {

-  font-size: 20pt; text-align: center; 

-}

-

-h5, h6, div.h7, div.h8, div.h9 {

-  font-size: 20pt;

-  border: 1px solid #000000;

-  margin-top: 5px;

-  margin-bottom: 2px;

-  text-align: center;

-  padding: 2px;

-}

-

-h5 {

-  background-color: #90FDFF;

-}

-

-h6 {

-  background-color: #016699;

-  color: white;

-}

-

-div.h7 {

-  background-color: #E0FFFF;

-}

-

-div.h8 {

-  background-color: #F0FFFF;

-}

-

-div.h9 {

-  background-color: #FFFFFF;

-}

-

-.typetable, .indextable, .paramstable {

-  border-style: hidden;

-}

-

-.paramstable {

-  padding: 5pt 5pt;

-}

-

-body {

-  background-color: white;

-}

-

-tr {

-  background-color: white;

-}

-

-td.typefieldcomment {

-  background-color: #FFFFFF;

-  font-size: smaller;

-}

-

-pre {

-  margin-bottom: 4px;

-}

-

-div.sig_block {

-  margin-left: 2em;

-}

-

-

-h2 {

-  font-family: Arial, Helvetica, sans-serif;

-  font-size: 16pt;

-  font-weight: normal;

-  border-bottom: 1px solid #dadada;

-  border-top: 1px solid #dadada;

-  color: #101010;

-  background: #eeeeff;

-  margin: 25px 0px 10px 0px;

-  padding: 1px 1px 1px 1px;

-}

-

-h3 {

-  font-family: Arial, Helvetica, sans-serif;

-  font-size: 12pt;

-  color: #016699;

-  font-weight: bold;

-  padding: 15px 0 0 0ex;

-  margin: 5px 0 0 0;

-}

-

-h4 {

-  font-family: Arial, Helvetica, sans-serif;

-  font-size: 10pt;

-  color: #016699;

-  padding: 15px 0 0 0ex;

-  margin: 5px 0 0 0;

-}

-

-/* Here starts the overwrite of default rules to give a better look */

-

-body {

-  font-family: Calibri, Georgia, Garamond, Baskerville, serif;

-  font-size: 12pt;

-  background-color: white;

-}

-

-a:link, a {

-  color: #6895c3 !important;

-}

-

-a:hover {

-  color: #2F4459 !important;

-  background-color: white;

-}

-

-hr {

-  height: 1px;

-  color: #016699;

-  background-color: #016699;

-  border-width: 0;

-}

-

-h1, h1 a:link, h1 a:visited, h1 a {

-  font-family: Cambria, Georgia, Garamond, Baskerville, serif;

-  color: #016699;

-}

-

-.navbar {

-  float: left;

-}

-

-.navbar a, .navbar a:link, .navbar a:visited {

-  color: #016699;

-  font-family: Arial, Helvetica, sans-serif;

-  font-weight: bold;

-  font-size: 80%;

-}

-

-.keyword {

-  color: #c13939;

-}

-

-.constructor {

-  color: #3c8f7e;

-}

-

-pre, code {

-  font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;

-  white-space: normal;

-  font-size: 9pt;

-  font-weight: bold;

-}

-

-.type br {

-  display: none;

-}

-

-.info {

-  margin-left: 1em;

-  font-size: 12pt;

-}