diff options
| author | Gaëtan Gilbert | 2020-03-26 15:08:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-26 15:08:52 +0100 |
| commit | fde8e449ca4a796e7dee55c6a518e8161e448f23 (patch) | |
| tree | f817534cad8fc19f6f3c2867936a5c792c0dfc74 | |
| parent | 53a84d4e84034d213e86839d05b87a5cd80b4181 (diff) | |
| parent | 5b726cdd242549fd292bc24b6e56073a16e8cf32 (diff) | |
Merge PR #11919: Remove outdated mention of -allow-sprop.
Reviewed-by: SkySkimmer
| -rw-r--r-- | doc/sphinx/language/cic.rst | 3 |
1 files changed, 1 insertions, 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. |