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 /doc | |
| 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").
Diffstat (limited to 'doc')
| -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: |