diff options
| author | Matej Kosik | 2015-10-29 14:05:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:09 +0100 |
| commit | cdd31465cee9ea8bef2a253280ee8a9647ecc01d (patch) | |
| tree | 0ccb399c0efff32abe3f2742b78c5357eb2584c0 | |
| parent | 3cebb15d999e6e26a98339ecb6fa7e62fdcf6a88 (diff) | |
SILENT: the anchor for the 'Local context' was moved to a more appropriate place.
| -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 |