diff options
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index e33f9cce7..f50c4fe1f 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -282,7 +282,7 @@ declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is declared in $E$, we write $(c : T) \in E$. \paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}} -In the following, we assume $E$ is a valid environment wrt to +In the following, we assume $E$ is a valid environment w.r.t. inductive definitions. We define simultaneously two judgments. The first one \WTEG{t}{T} means the term $t$ is well-typed and has type $T$ in the environment $E$ and context $\Gamma$. The |