small corrections

doc/chapter-primrec.tex

@@ -879,15 +879,18 @@ \subsection{Looking for a contradiction}
 Thus, our impossibility proof is just a sequence of easy small steps.
 
 \begin{remark}
-In the following snippet,  \emph{Alectryon}'s \texttt{Latex} generator  prints the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}.
+In the following snippet,  some versions \emph{Alectryon}'s \texttt{Latex} generator  print the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}.
 Thus the proof script is correct, but the three last sub-goals are not correctly displayed, since 
 they do not show how the inequalities $2\leq x$ and $m \leq x$ could be inferred by \texttt{lia}.
+
+A correct goal display can be obtained with
+\href{https://github.com/Casteran/alectryonFix}{this fork}.
 \end{remark}
 
 \input{movies/snippets/AckNotPR/AckNotPR}
 
 \begin{remark}
-It is easy to prove that any unary function which dominates \texttt{fun n => Ack n n} fails to be primitive recursive. To this end, we use an instance of \texttt{majorAnyPR} dealing with unary functions.
+It is easy to prove that any unary function which dominates (\texttt{fun n => Ack n n}) fails to be primitive recursive. To this end, we use an instance of \texttt{majorAnyPR} dealing with unary functions.
 
 \vspace{4pt}
 \noindent