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/addendum/sprop.rst | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9a9ec78edc..9acdd18b89 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -9,9 +9,11 @@ SProp (proof irrelevant propositions)
 
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
-known as strict propositions). Using :math:`\SProp` may be prevented
-by passing ``-disallow-sprop`` to the |Coq| program or using
-:flag:`Allow StrictProp`.
+known as strict propositions) as described in
+:cite:`Gilbert:POPL2019`.
+
+Using :math:`\SProp` may be prevented by passing ``-disallow-sprop``
+to the |Coq| program or using :flag:`Allow StrictProp`.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
-- 
cgit v1.2.3