From ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 1 Sep 2018 12:39:09 -0700
Subject: Rewrite "Flags, Options and Tables" section. Mark boolean-valued
 options with :flag: Adjust tactic and command names so parameters aren't
 shown in the index unless they're needed for disambiguation. Remove
 references to synchronous options. Revise doc for tables. Correct indentation
 for text below :flag:

---
 doc/sphinx/language/cic.rst | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'doc/sphinx/language/cic.rst')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index c8c3e37efb..381f8bb661 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1025,21 +1025,21 @@ Template polymorphism
 Inductive types can be made polymorphic over their arguments
 in :math:`\Type`.
 
-.. opt:: Auto Template Polymorphism
+.. flag:: Auto Template Polymorphism
 
-  This option, enabled by default, makes every inductive type declared
-  at level :math:`Type` (without annotations or hiding it behind a
-  definition) template polymorphic.
+   This option, enabled by default, makes every inductive type declared
+   at level :math:`Type` (without annotations or hiding it behind a
+   definition) template polymorphic.
 
-  This can be prevented using the ``notemplate`` attribute.
+   This can be prevented using the ``notemplate`` attribute.
 
-  An inductive type can be forced to be template polymorphic using the
-  ``template`` attribute.
+   An inductive type can be forced to be template polymorphic using the
+   ``template`` attribute.
 
-  Template polymorphism and universe polymorphism (see Chapter
-  :ref:`polymorphicuniverses`) are incompatible, so if the later is
-  enabled it will prevail over automatic template polymorphism and
-  cause an error when using the ``template`` attribute.
+   Template polymorphism and universe polymorphism (see Chapter
+   :ref:`polymorphicuniverses`) are incompatible, so if the later is
+   enabled it will prevail over automatic template polymorphism and
+   cause an error when using the ``template`` attribute.
 
 If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
@@ -1120,7 +1120,7 @@ and otherwise in the Type hierarchy.
 
 Note that the side-condition about allowed elimination sorts in the
 rule **Ind-Family** is just to avoid to recompute the allowed elimination
-sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). As
+sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As
 an example, let us consider the following definition:
 
 .. example::
@@ -1244,7 +1244,7 @@ primitive recursion over the structure.
 But this operator is rather tedious to implement and use. We choose in
 this version of |Coq| to factorize the operator for primitive recursion
 into two more primitive operations as was first suggested by Th.
-Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The
+Coquand in :cite:`Coq92`. One is the definition by pattern matching. The
 second one is a definition by guarded fixpoints.
 
 
-- 
cgit v1.2.3