diff --git a/spec/doc.tex b/spec/doc.tex
index 50ca0aa7f5e75867917e3fc6be3056c9276d917f..6f50f5d9807d4a74d3a5dd17b7c6de71c344696b 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -704,7 +704,9 @@ An Alethe proof is a list of commands.
  \grNT{clause}          &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
  \grNT{proof\_term}     &\grRule & \grNT{term}\text{ extended with } \\
                         &        & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)}  \\
-                        & \grOr  & \grNT{rational}\;\grOr\;\grNT{neg\_numeral}\;\grOr\;\grNT{neg\_decimal} \\
+                        & \grOr  & \grNT{rational} \\
+                        & \grOr  & \grNT{nonpositive\_numeral} \\
+                        & \grOr  & \grNT{nonpositive\_decimal} \\
  \grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
  \grNT{args\_annotation}     &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)}  \\
  \grNT{step\_arg}            &\grRule & \grNT{symbol}\;\grOr\;
@@ -714,8 +716,8 @@ An Alethe proof is a list of commands.
                              & \grOr  & \textAlethe{(:=}\, \grNT{sorted\_var}\;\grNT{proof\_term}\,\textAlethe{)} \\
  \grNT{positive\_numeral}    &\grRule & \text{any }\grNT{numeral}\text{ except } 0\\
  \grNT{rational}             &\grRule & -^{?}\grNT{numeral}/\grNT{positive\_numeral} \\
- \grNT{negative\_numeral}         &\grRule & -\grNT{numeral} \\
- \grNT{negative\_decimal}        &\grRule & -\grNT{decimal} \\
+ \grNT{nonpositive\_numeral}         &\grRule & -\grNT{numeral} \\
+ \grNT{nonpositive\_decimal}        &\grRule & -\grNT{decimal} \\
   \end{array}
   \]
   \caption{The proof grammar.}
@@ -818,14 +820,14 @@ For example, $-\frac{1}{2}$ is written as
 \inlineAlethe{(/ (- 1) 2)}.
 The $\grNT{rational}$ non-terminal makes it possible to write this constant
 as a single literal: \inlineAlethe{-1/2}.
-Furthermore, the non-terminals $\grNT{negative\_numeral}$ and $\grNT{negative\_decimal}$
+Furthermore, the non-terminals $\grNT{nonpositive\_numeral}$ and $\grNT{nonpositive\_decimal}$
 achieve the same for unary negation.
 
 The sorting rules for $\grNT{proof\_term}$ are as for {\smtlib} terms with
 one key difference.
 The sort of terms produced by $\grNT{rational}$, $\grNT{decimal}$, and
-$\grNT{negative\_decimal}$ is always \inlineAlethe{Real}.
-The sort of terms produced by $\grNT{integer}$ and $\grNT{negative\_numeral}$
+$\grNT{nonpositive\_decimal}$ is always \inlineAlethe{Real}.
+The sort of terms produced by $\grNT{integer}$ and $\grNT{nonpositive\_numeral}$
 is always \inlineAlethe{Int}.
 For example, in standard {\smtlib}, the term \inlineAlethe{(+ 5 3)}
 has the sort \inlineAlethe{Int} in the logic \texttt{QF\_LIA}, but
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index ca7d00d0c5865c33031a658c27f4eff1cbb4a42c..c226703eb54b2cc2a969770ef5910cc7ccfc8d56 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -429,7 +429,7 @@ where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
 
 The constants $a_i$ are of sort \inlineAlethe{Real} and must be printed
 using one of the productions $\grNT{rational}$
-$\grNT{decimal}$, $\grNT{negative\_decimal}$.
+$\grNT{decimal}$, $\grNT{nonpositive\_decimal}$.
 
 To check the unsatisfiability of the negation of $\varphi_1\lor \dots
 \lor \varphi_o$ one performs the following steps for each literal. For