Replace Coq by Rocq

The Coq programing language was renamed to Rocq. The first occurrence
of the new name give the former name in a footnote.

Author: Arthur-Milchior

src/content/1.9/function-types.tex

@@ -582,15 +582,15 @@ \section{Curry-Howard Isomorphism}
 
 These are all interesting examples, but is there a practical side to
 Curry-Howard isomorphism? Probably not in everyday programming. But
-there are programming languages like Agda or Coq, which take advantage
+there are programming languages like Agda or Rocq\footnote{Formerly known as Coq}, which take advantage
 of the Curry-Howard isomorphism to prove theorems.
 
 Computers are not only helping mathematicians do their work --- they are
 revolutionizing the very foundations of mathematics. The latest hot
 research topic in that area is called Homotopy Type Theory, and is an
 outgrowth of type theory. It's full of Booleans, integers, products and
 coproducts, function types, and so on. And, as if to dispel any doubts,
-the theory is being formulated in Coq and Agda. Computers are
+the theory is being formulated in Rocq and Agda. Computers are
 revolutionizing the world in more than one way.
 
 \section{Bibliography}

src/content/2.4/representable-functors.tex

@@ -31,7 +31,7 @@
 latest branch of mathematics, the Homotopy Type Theory (HoTT). I'm
 mentioning HoTT because it's a pure mathematical theory that takes
 inspiration from computation, and one of its main proponents, Vladimir
-Voevodsky, had a major epiphany while studying the Coq theorem prover.
+Voevodsky, had a major epiphany while studying the Rocq theorem prover.
 The interaction between mathematics and programming goes both ways.
 
 The important lesson about sets is that it's okay to compare sets of