Apply suggested changes by Guillaume. Also, the exn block

rather primarily belongs to Extract Constant cmd as the inlining variant
is syntactic sugar only.

doc/sphinx/addendum/extraction.rst

@@ -295,22 +295,21 @@ what ML term corresponds to a given axiom.
         Axiom Y : Set -> Set -> Set.
         Extract Constant Y "'a" "'b" => " 'a * 'b ".
 
+   .. note::
+      The extraction recognizes whether the realized axiom
+      should become a ML type constant or a ML object declaration. For example:
 
-.. cmd:: Extract Inlined Constant @qualid => {| @ident | @string }
-
-   Same as the previous one, except that the given ML terms will
-   be inlined everywhere instead of being declared via a ``let``.
+      .. coqtop:: in
 
-   .. note::
-      This command is sugar for an :cmd:`Extract Constant` followed
-      by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline`
-      will have an effect on the realized and inlined axiom.
+         Axiom X:Set.
+         Axiom x:X.
+         Extract Constant X => "int".
+         Extract Constant x => "0".
 
    .. caution:: It is the responsibility of the user to ensure that the ML
       terms given to realize the axioms do have the expected types. In
       fact, the strings containing realizing code are just copied to the
-      extracted files. The extraction recognizes whether the realized axiom
-      should become a ML type constant or a ML object declaration. For example:
+      extracted files.
 
    .. exn:: The term @qualid is already defined as foreign custom constant.
 
@@ -319,12 +318,15 @@ what ML term corresponds to a given axiom.
       for :n:`@qualid` would override this command.
 
 
-.. coqtop:: in
+.. cmd:: Extract Inlined Constant @qualid => {| @ident | @string }
+
+   Same as the previous one, except that the given ML terms will
+   be inlined everywhere instead of being declared via a ``let``.
 
-   Axiom X:Set.
-   Axiom x:X.
-   Extract Constant X => "int".
-   Extract Constant x => "0".
+   .. note::
+      This command is sugar for an :cmd:`Extract Constant` followed
+      by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline`
+      will have an effect on the realized and inlined axiom.
 
 Realizing an axiom via :cmd:`Extract Constant` is only useful in the
 case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom