CLEANUP PROPOSITION: rephrasing the original idea in a simpler way

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e5307ef1ec..2a4ccfed87 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -242,7 +242,7 @@ either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such
 that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some
 $x:=t:T$, we also write $(x:=t:T) \in \Gamma$.
 For the rest of the chapter, the
-notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the local context
+notation $\Gamma::(y:T)$ (resp.\ $\Gamma::(y:=t:T)$) denotes the local context
 $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
 notation $[]$ denotes the empty local context.
 
@@ -1708,7 +1708,7 @@ The typing rule is the expected one for a fixpoint.
 \end{description}
 
 Any fixpoint definition cannot be accepted because non-normalizing terms
-will lead to proofs of absurdity.
+allow proofs of absurdity.
 
 The basic scheme of recursion that should be allowed is the one needed for 
 defining primitive