Complete a remark in Chapter 11 (Alectryon output)

coq-community · Nov 29, 2023 · a0f1149 · a0f1149
1 parent ed21e44
commit a0f1149
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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