From b23331eb03f2640e85bd65277c15a4bcc692b90c Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 09:50:11 +0100
Subject: ENH: citation

---
 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 c481b3adba..2c0f155388 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -44,7 +44,7 @@ function types over these data types.
 
 {\Prop} and {\Set} themselves can be manipulated as ordinary
 terms. Consequently they also have a type. Because assuming simply
-that {\Set} has type {\Set} leads to an inconsistent theory, the
+that {\Set} has type {\Set} leads to an inconsistent theory~\cite{Coq86}, the
 language of {\CIC} has infinitely many sorts. There are, in addition
 to {\Set} and {\Prop} a hierarchy of universes {\Type$(i)$} for any
 integer $i$.
-- 
cgit v1.2.3