diff options
| -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 04df208ee2..690bdad950 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -226,7 +226,7 @@ As objects of type theory, terms are subjected to {\em type discipline}. The well typing of a term depends on a global environment and a local context. -\paragraph{Local context.} +\paragraph{Local context.\index{Local context}} A {\em local context} is an ordered list of local declarations of names which we call {\em variables}. The declaration of some variable $x$ is @@ -241,7 +241,7 @@ $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 $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The -notation $[]$ denotes the empty local context. \index{Local context} +notation $[]$ denotes the empty local context. % Does not seem to be used further... % Si dans l'explication WF(E)[Gamma] concernant les constantes |