aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-cic.tex
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-24 13:50:08 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:20 +0100
commitf43f474fe3ba0b01115ef02b0032f706879ee521 (patch)
tree92a9c6e02dcd1eee3d62988162528bb1502b735a /doc/refman/RefMan-cic.tex
parent6fa4d20b5208852ac468c28405e93bcb5288d774 (diff)
FIX: wrong reference to a figure
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
-rw-r--r--doc/refman/RefMan-cic.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ad711549b..1b461afcb 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -532,7 +532,7 @@ These inductive definitions, together with global assumptions and global definit
Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$
such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as:
$\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}.
-Figures~\ref{fig:bool}--\ref{fig:even:odd} show formal representation of several inductive definitions.
+Figures~\ref{fig:bool}--\ref{fig:tree:forest} show formal representation of several inductive definitions.
\begin{latexonly}%
\newpage