From 1372e075c52aa2dad547a42eaf9aba1f83a7abb1 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 13:47:27 +0100
Subject: CLEANUP PROPOSITION: this sentence does not help us to better
 understand the semantics of the language

---
 doc/refman/RefMan-cic.tex | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ed7889e480..fb6a5bff83 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -181,8 +181,7 @@ More precisely the language of the {\em Calculus of Inductive
 \paragraph{Free variables.}
 The notion of free variables is defined as usual.  In the expressions
 $\lb x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$
-are bound.  They are represented by de Bruijn indexes in the internal
-structure of terms.
+are bound.
 
 \paragraph[Substitution.]{Substitution.\index{Substitution}}
 The notion of substituting a term $t$ to free occurrences of a
-- 
cgit v1.2.3