From 5a2c2febd2c963e58142edaf809f0a4cac806561 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 30 Oct 2025 13:59:51 +0100
Subject: Note Coq→Rocq name change.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 transp-inf110-02-typage.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'transp-inf110-02-typage.tex')

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 9082576..71547c7 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -562,7 +562,7 @@ fonctions p.r.
 
 \bigskip
 
-Exemple de tel langage : Coq.
+Exemple de tel langage : Coq (maintenant appelé Rocq).
 
 \end{frame}
 %
@@ -716,7 +716,7 @@ tacite qu'on peut construire un tel $A$.
 \itempoint Langages spécialisés pour servir à la fois à l'écriture de
 programmes informatiques et de preuves mathématiques ; ils peuvent
 être soit sous forme de systèmes abstraits, soit sous forme
-d'implémentation informatique (« assistants de preuve » : Coq, Agda,
+d'implémentation informatique (« assistants de preuve » : Coq/Rocq, Agda,
 Lean…).
 
 \bigskip
@@ -769,7 +769,7 @@ n'a aucune des trois, CoC a les trois) :
 \medskip
 
 {\footnotesize On peut ensuite encore ajouter des fonctionnalités :
-  par exemple, Coq est basé sur le « calcul des constructions
+  par exemple, Coq/Rocq est basé sur le « calcul des constructions
   inductives » qui ajoute au calcul des constructions des mécanismes
   systématiques pour former des types (positivement !) récursifs.\par}
 
-- 
cgit v1.2.3

