diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 3 |
1 files changed, 1 insertions, 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 |