diff --git a/books/free-programming-books-fr.md b/books/free-programming-books-fr.md
index ddaa97b9b..f81be5362 100644
--- a/books/free-programming-books-fr.md
+++ b/books/free-programming-books-fr.md
@@ -15,7 +15,6 @@
 * [C / C++](#c--c)
 * [Caml / OCaml](#caml--ocaml)
 * [Chaîne de blocs / Blockchain](#chaîne-de-blocs--blockchain)
-* [Coq](#coq)
 * [Fortran](#fortran)
 * [Git](#git)
 * [Go](#go)
@@ -41,6 +40,7 @@
 * [Python](#python)
     * [Django](#django)
 * [R](#r)
+* [Rocq Prover](#rocq-prover)
 * [Ruby](#ruby)
 * [Rust](#rust)
 * [Sage](#sage)
@@ -139,11 +139,6 @@
 * [Maîtriser Ethereum: Développer des contrats intelligents et des DApps](https://ethereum.maitriser.ca) - Andreas M. Antonopoulos, Gavin Wood, Serafim Dos Santos (asciidoc, HTML)
 
 
-### Coq
-
-* [Le Coq'Art (V8)](http://www.labri.fr/perso/casteran/CoqArt/) - Yves Bertot, Pierre Castéran
-
-
 ### Fortran
 
 * [IDRIS adaptation of the Fortran 77 manual](http://www.idris.fr/formations/fortran/fortran-77.html) - IDRIS, Hervé Delouis, Patrick Corde (HTML)
@@ -296,6 +291,11 @@
 * [Introduction à la programmation en R](http://cran.r-project.org/doc/contrib/Goulet_introduction_programmation_R.pdf) - Vincent Goulet (PDF)
 
 
+### Rocq Prover
+
+* [Le Coq'Art (V8)](http://www.labri.fr/perso/casteran/CoqArt/) - Yves Bertot, Pierre Castéran
+
+
 ### Ruby
 
 * [Ruby en vingt minutes](https://www.ruby-lang.org/fr/documentation/quickstart/)
diff --git a/books/free-programming-books-ja.md b/books/free-programming-books-ja.md
index fc20f39af..e57afe72e 100644
--- a/books/free-programming-books-ja.md
+++ b/books/free-programming-books-ja.md
@@ -29,7 +29,6 @@
 * [C++](#cpp)
 * [Clojure](#clojure)
 * [CoffeeScript](#coffeescript)
-* [Coq](#coq)
 * [D](#d)
 * [Elixir](#elixir)
 * [Erlang](#erlang)
@@ -69,6 +68,7 @@
 * [Python](#python)
     * [Flask](#flask)
 * [R](#r)
+* [Rocq Prover](#rocq-prover)
 * [Ruby](#ruby)
 * [Rust](#rust)
 * [Sather](#sather)
@@ -304,11 +304,6 @@
 * [正規表現リファレンス（CoffeeScript)](https://kyu-mu.net/coffeescript/regexp) - 飯塚直
 
 
-### Coq
-
-* [ソフトウェアの基礎](http://proofcafe.org/sf) - Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey, `trl:` 梅村晃広, `trl:` 片山功士, `trl:` 水野洋樹, `trl:` 大橋台地, `trl:` 増子萌, `trl:` 今井宜洋
-
-
 ### D
 
 * [D言語基礎文法最速マスター](https://gist.github.com/repeatedly/2470712) - Masahiro Nakagawa
@@ -611,6 +606,11 @@
 * [無料統計ソフトRで心理学](http://blue.zero.jp/yokumura/Rhtml/Haebera2002.html) - 奥村泰之
 
 
+### Rocq Prover
+
+* [ソフトウェアの基礎](http://proofcafe.org/sf) - Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey, `trl:` 梅村晃広, `trl:` 片山功士, `trl:` 水野洋樹, `trl:` 大橋台地, `trl:` 増子萌, `trl:` 今井宜洋
+
+
 ### Ruby
 
 * [Ruby on Rails ガイド](https://railsguides.jp) - Rails community, `trl:` 八田 昌三, `trl:` 安川 要平
diff --git a/books/free-programming-books-langs.md b/books/free-programming-books-langs.md
index 3d153e7eb..e8fcb4ec1 100644
--- a/books/free-programming-books-langs.md
+++ b/books/free-programming-books-langs.md
@@ -40,7 +40,6 @@ Books on general-purpose programming that don't focus on a specific language are
 * [ColdFusion](#coldfusion)
 * [Component Pascal](#component-pascal)
 * [Cool](#cool)
-* [Coq](#coq)
 * [Crystal](#crystal)
 * [CUDA](#cuda)
 * [D](#d)
@@ -186,6 +185,7 @@ Books on general-purpose programming that don't focus on a specific language are
 * [Raku](#raku)
 * [Raspberry Pi](#raspberry-pi)
 * [REBOL](#rebol)
+* [Rocq Prover](#rocq-prover)
 * [Ruby](#ruby)
     * [RSpec](#rspec)
     * [Ruby on Rails](#ruby-on-rails)
@@ -639,8 +639,7 @@ Books on general-purpose programming that don't focus on a specific language are
 
 ### Coq
 
-* [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/html/toc.html)
-* [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/)
+> :information_source: (renamed) see [Rocq Prover](#roq-prover)
 
 
 ### Crystal
@@ -2327,6 +2326,12 @@ Books on general-purpose programming that don't focus on a specific language are
 * [Sinatra Book](https://github.com/sinatra/sinatra-book)
 
 
+### Rocq Prover
+
+* [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/html/toc.html)
+* [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/)
+
+
 ### Rust
 
 * [A Gentle Introduction To Rust](https://stevedonovan.github.io/rust-gentle-intro) - Steve J Donovan