From 43816ce712054c07cb04452821570054aff3dc44 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 7 Nov 2015 15:37:39 +0100
Subject: CLEANUP PROPOSITION: rephrasing the original idea in a simpler way

---
 doc/refman/RefMan-cic.tex | 4 ++--
 1 file 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
-- 
cgit v1.2.3