diff options
| author | Matej Kosik | 2015-10-29 10:22:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:08 +0100 |
| commit | 950dace27c3233f740b2031c9d99cb3f155aefbf (patch) | |
| tree | 08565011edd7eecf02354fa27d93c387d22d5e2c | |
| parent | 0117f54f3e3678f348f8ed84c8444dc614ce8298 (diff) | |
ENH: Index anchor repositioning.
Originally, when user clicked in index on "Type", he landed
on an incorrect page (immediatelly following the page
which actually contains the definition of "Type").
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 505587988c..702adc2326 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -56,10 +56,10 @@ sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all products, subsets and function types over these sorts. Formally, we call {\Sort} the set of sorts which is defined by: +\index{Type@{\Type}}% +\index{Prop@{\Prop}}% +\index{Set@{\Set}}% \[\Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i \in \NN\} \] -\index{Type@{\Type}} -\index{Prop@{\Prop}} -\index{Set@{\Set}} Their properties are defined in Section~\ref{subtyping-rules}. % TODO: Somewhere in the document we should explain: |