Note Coq→Rocq name change.

2 files changed, 4 insertions, 4 deletions

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}
 
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 07c5d43..61063b9 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -542,7 +542,7 @@ monde des démonstrations, plus simples, ou différentes.
 
 \medskip
 
-\itempoint En Coq, les deux mondes sont \alert{séparés mais
+\itempoint En Coq/Rocq, les deux mondes sont \alert{séparés mais
   parallèles} : $\mathit{Prop}$ pour le type des propositions et
 $\mathit{Type}$ pour le type des types d'individus.