From cdd31465cee9ea8bef2a253280ee8a9647ecc01d Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 14:05:50 +0100
Subject: SILENT: the anchor for the 'Local context' was moved to a more
 appropriate place.

---
 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 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
-- 
cgit v1.2.3