1 files changed, 11 insertions, 10 deletions

diff --git a/controle-20250129.tex b/controle-20250129.tex
index c5a76cc..2c165b0 100644
--- a/controle-20250129.tex
+++ b/controle-20250129.tex
@@ -86,14 +86,16 @@ du problème) présentent une gradation approximative de difficulté, il
 est recommandé de les traiter dans l'ordre.
 
 La longueur du sujet ne doit pas effrayer : l'énoncé du problème est
-très long parce que des rappels ont été faits et que les questions ont
-été rédigées de façon aussi précise que possible.  Par ailleurs, il ne
-sera pas nécessaire de tout traiter pour avoir le maximum des points.
+très long parce que des rappels et éclaircissements ont été faits et
+que les questions ont été rédigées de façon aussi précise que
+possible.  Par ailleurs, il ne sera pas nécessaire de tout traiter
+pour avoir le maximum des points.
 
 \medbreak
 
-Les exercices 1 à 4 portent sur Coq.  L'exercice 5 porte sur le calcul
-propositionnel.  Le problème final porte sur la calculabilité.
+Dans les exercices portant sur Coq (exercices 1 à 4), les erreurs de
+syntaxe Coq ne seront pas pénalisées tant qu'on comprend clairement
+l'intention.
 
 \medbreak
 
@@ -106,13 +108,10 @@ L'usage des appareils électroniques est interdit.
 
 Durée : 3h
 
-Barème \emph{approximatif} et \emph{indicatif} (sur $20$) :
-\textcolor{red}{à écrire}.
-
 \ifcorrige
-Ce corrigé comporte 14 pages \textcolor{red}{(à revérifier)} (page de garde incluse).
+Ce corrigé comporte 15 pages (page de garde incluse).
 \else
-Cet énoncé comporte 8 pages \textcolor{red}{(à revérifier)} (page de garde incluse).
+Cet énoncé comporte 8 pages (page de garde incluse).
 \fi
 
 \vfill
@@ -575,6 +574,8 @@ l'applique à $\langle c,c\rangle$ avec $c$ le code de Gödel d'une
 fonction constante quelconque, et que pour $A=\varnothing$ et
 $B=\mathbb{N}$ il doit renvoyer $\langle 1,\emdash\rangle$.)
 
+\smallskip
+
 La formule en question est-elle démontrable en calcul propositionnel
 classique ?  (On ne demande pas forcément d'en exhiber une
 démonstration.)