From 8cc98698e8fc2cf86c5173c2dc0834538a2ca075 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Sun, 29 Apr 2018 23:19:10 -0400
Subject: [doc] Small fixes

---
 doc/sphinx/addendum/micromega.rst | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index f887a5feea..0e9c23b9bb 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin
 
 .. _ceil_thm:
 
-**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then
+.. thm:: Bound on the ceiling function
 
- :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`
+   Let :math:`p` be an integer and :math:`c` a rational constant. Then
+   :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
 
 For instance, from 2 x = 1 we can deduce
 
-- 
cgit v1.2.3


From d5bb8a4ae2f509532ecfb4a53bb91c64d992c2e6 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 4 May 2018 19:02:11 -0400
Subject: [doc] Address feedback on doc writer guide

Co-Authored-By: @Zimmi48
---
 doc/sphinx/addendum/implicit-coercions.rst | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 152f4f6552..09faa06765 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -140,29 +140,29 @@ Declaration of Coercions
 
   .. warn:: Ambiguous path.
 
-    When the coercion `qualid` is added to the inheritance graph, non
-    valid coercion paths are ignored; they are signaled by a warning
-    displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+     When the coercion :token:`qualid` is added to the inheritance graph, non
+     valid coercion paths are ignored; they are signaled by a warning
+     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
-    Declares the construction denoted by `qualid` as a coercion local to
-    the current section.
+     Declares the construction denoted by `qualid` as a coercion local to
+     the current section.
 
   .. cmdv:: Coercion @ident := @term
 
-    This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
   .. cmdv:: Coercion @ident := @term : @type
 
-    This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
   .. cmdv:: Local Coercion @ident := @term
 
-    This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
 Assumptions can be declared as coercions at declaration time.
 This extends the grammar of assumptions from
-- 
cgit v1.2.3