From d3a193260bfa28c9205c64718f6a4c57ee17ea0a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 4 Nov 2019 16:23:38 +0100
Subject: Cite POPL19 SProp paper

Close #10242
---
 doc/sphinx/language/cic.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 6410620b40..f659438674 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -49,7 +49,8 @@ The sort :math:`\SProp` is like :math:`\Prop` but the propositions in
 equal). Objects of type :math:`\SProp` are called strict propositions.
 :math:`\SProp` is rejected except when using the compiler option
 ``-allow-sprop``. See :ref:`sprop` for information about using
-:math:`\SProp`.
+:math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
+considerations.
 
 The sort :math:`\Set` intends to be the type of small sets. This includes data
 types such as booleans and naturals, but also products, subsets, and
-- 
cgit v1.2.3