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(-)

(limited to 'programme-inf110.tex')

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


From 04d6647251c905e8ec50f86eef3bd801844a9796 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 24 Jan 2025 12:33:01 +0100
Subject: Clarify wording.

---
 programme-inf110.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'programme-inf110.tex')

diff --git a/programme-inf110.tex b/programme-inf110.tex
index c42d6ef..855b070 100644
--- a/programme-inf110.tex
+++ b/programme-inf110.tex
@@ -77,7 +77,7 @@ Git: \input{vcline.tex}
   propositionnel intuitionniste.
 \item \textbf{Calcul propositionnel :} règles de logique en déduction
   naturelle, et au moins une présentation des preuves (arbre de
-  séquents, ou drapeau) ; écriture et vérification des
+  preuve, ou drapeau) ; écriture et vérification des
   $\lambda$-termes de preuve (sans entrer dans le détail pointilleux
   des notations) ; différence entre logique intuitionniste et logique
   classique ; propriété de la disjonction et décidabilité du calcul
-- 
cgit v1.2.3

