From 7c645566ef64f09bd6c80007c9e66305ccb90659 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 15:16:46 +0100
Subject: Fix \label which was meants to be \ref in doc of CIC terms.

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e3e49e115d..1554ee04d3 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -24,7 +24,7 @@ written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as
 The types of types are {\em sorts}. Types and sorts are themselves
 terms so that terms, types and sorts are all components of a common
 syntactic language of terms which is described in
-Section~\label{cic:terms} but, first, we describe sorts.
+Section~\ref{cic:terms} but, first, we describe sorts.
 
 \subsection[Sorts]{Sorts\label{Sorts}
 \index{Sorts}}
-- 
cgit v1.2.3