From 5b726cdd242549fd292bc24b6e56073a16e8cf32 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 26 Mar 2020 13:54:51 +0100
Subject: Remove outdated mention of -allow-sprop.

---
 doc/sphinx/language/cic.rst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b0acd09af6..09a3897a06 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -47,8 +47,7 @@ provable. An object of type :math:`\Prop` is called a proposition.
 The sort :math:`\SProp` is like :math:`\Prop` but the propositions in
 :math:`\SProp` are known to have irrelevant proofs (all proofs are
 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
+See :ref:`sprop` for information about using
 :math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
 considerations.
 
-- 
cgit v1.2.3