From 3c3883dc467f573a62e2c6c0a3908882aa52702d Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 24 Jan 2025 12:15:04 +0100
Subject: Clarify syllabus re Coq.

---
 programme-inf110.tex | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/programme-inf110.tex b/programme-inf110.tex
index c6217c7..c42d6ef 100644
--- a/programme-inf110.tex
+++ b/programme-inf110.tex
@@ -103,7 +103,11 @@ Git: \input{vcline.tex}
   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.
+  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 eCampus du cours).
 \end{itemize}
 
 \bigskip
-- 
cgit v1.2.3