From 61c780ad8138bfa768977d652c25741dad35d448 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 18 Apr 2019 14:26:39 +0200
Subject: First fixing pass, and experiment with dune-style PR number and
 author listing.

---
 doc/sphinx/addendum/sprop.rst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index c0c8c2d79c..8935ba27e3 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -10,9 +10,9 @@ 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). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`.
+``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
 
-.. opt:: Allow StrictProp
+.. flag:: Allow StrictProp
    :name: Allow StrictProp
 
    Allows using :math:`\SProp` when set and forbids it when unset. The
@@ -201,10 +201,10 @@ This means that some errors will be delayed until ``Qed``:
 
    Abort.
 
-.. opt:: Elaboration StrictProp Cumulativity
+.. flag:: Elaboration StrictProp Cumulativity
    :name: Elaboration StrictProp Cumulativity
 
-   Unset this option (it's on by default) to be strict with regard to
+   Unset this flag (it is on by default) to be strict with regard to
    :math:`\SProp` cumulativity during elaboration.
 
 The implementation of proof irrelevance uses inferred "relevance"
-- 
cgit v1.2.3