diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
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 |