diff --git a/doc/chapter-primrec.tex b/doc/chapter-primrec.tex
index 4c70cf24..6c67517f 100644
--- a/doc/chapter-primrec.tex
+++ b/doc/chapter-primrec.tex
@@ -866,7 +866,7 @@ \subsection{Looking for a contradiction}
 Thus, our impossibility proof is just a sequence of easy small steps.
 
 \begin{todo}
-Fix the display the local definition of \texttt{x} in the following proof.
+  Fix the display of the local definition of \texttt{x} in the following proof: \emph{Alectryon} prints a \emph{declaration} \texttt{x: nat}, but forgets to print the definition \texttt{x := Nat.max 2 m},  which is  important to complete the proof.
 \end{todo}
 
 \input{movies/snippets/AckNotPR/AckNotPR}
diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index b36c4331..d5fd3ecc 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -636,7 +636,7 @@ Fixpoint minus (alpha beta : T1) :T1 :=
      then zero
      else  cons zero (Peano.pred (n-n')) zero
  |  cons zero n _, zero =>  cons zero n zero
- |  cons zero n _, y =>  zero
+ |  cons zero _ _, _ =>  zero
  |  cons a n b, zero =>  cons a n b
  |  cons a n b, cons a' n' b' =>
      (match compare a a' with