From f6ff6ed8783096047432e8f1ec8f474a3d94422f Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 19 Jan 2026 12:45:37 +0100
Subject: Rocq is the new Coq.

---
 programme-inf110.tex | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/programme-inf110.tex b/programme-inf110.tex
index ff5bb1c..c4f964e 100644
--- a/programme-inf110.tex
+++ b/programme-inf110.tex
@@ -103,12 +103,12 @@ Git: \input{vcline.tex}
   est valable est décidable, mais que savoir si un énoncé est un
   théorème est seulement semi-décidable ; l'énoncé du théorème de
   Gödel et l'idée de sa démonstration.
-\item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée
-  en TP, et notamment les principales tactiques de raisonnement (sur
-  les connecteurs logiques, types inductifs, égalités, etc.).  Le nom
-  des tactiques est exigible donc on recommande de préparer un
-  récapitulatif pour l'examen (un tel document est disponible sur la
-  page Moodle du cours).
+\item \textbf{Coq/Rocq :} l'utilisation générale de Coq/Rocq telle que
+  pratiquée en TP, et notamment les principales tactiques de
+  raisonnement (sur les connecteurs logiques, types inductifs,
+  égalités, etc.).  Le nom des tactiques est exigible donc on
+  recommande de préparer un récapitulatif pour l'examen (un tel
+  document est disponible sur la page Moodle du cours).
 \end{itemize}
 
 \bigskip
@@ -124,12 +124,12 @@ Git: \input{vcline.tex}
   combinateur $\mathsf{Z}$ ou sa différence avec $\mathsf{Y}$.
 \item Les détails du typage de quelque langage de programmation que ce
   soit (autres que les variantes du $\lambda$-calcul simplement typé
-  vus en cours, et les parties de Coq vues en TP), notamment rien de
-  ce qui concerne Scheme, Haskell ou quelque autre langage mentionné
-  en passant dans le cours ; le sous-typage, le polymorphisme ad hoc,
-  les types dépendants, ou les autres fonctionnalités de certains
-  systèmes de typages mentionnés en passant dans le cours.
-  L'algorithme de Hindley-Milner.
+  vus en cours, et les parties de Coq/Rocq vues en TP), notamment rien
+  de ce qui concerne Scheme, Haskell ou quelque autre langage
+  mentionné en passant dans le cours ; le sous-typage, le
+  polymorphisme ad hoc, les types dépendants, ou les autres
+  fonctionnalités de certains systèmes de typages mentionnés en
+  passant dans le cours.  L'algorithme de Hindley-Milner.
 \item Le calcul des séquents, le fonctionnement de l'élimination des
   coupures ou sa preuve.  Le $\overline{\lambda}$-calcul.  Les axiomes
   de Hilbert, et les combinateurs $\mathsf{S},\mathsf{K},\mathsf{I}$.
@@ -149,7 +149,7 @@ Git: \input{vcline.tex}
   l'absurde).
 \item Les détails de la démonstration du théorème de Gödel, la
   formalisation des systèmes précis auxquels il s'applique.
-\item Les détails de la syntaxe de Coq.
+\item Les détails de la syntaxe de Coq/Rocq.
 \end{itemize}
 
 
-- 
cgit v1.2.3