Apply another review suggestion by Guillaume. Also, fixing a typo.

doc/sphinx/addendum/extraction.rst

@@ -311,13 +311,6 @@ what ML term corresponds to a given axiom.
       fact, the strings containing realizing code are just copied to the
       extracted files.
 
-   .. exn:: The term @qualid is already defined as foreign custom constant.
-
-      The :n:`@qualid` was previously used in a
-      :cmd:`Extract Foreign Constant` command. Using :cmd:`Extract Inlined Constant`
-      for :n:`@qualid` would override this command.
-
-
 .. cmd:: Extract Inlined Constant @qualid => {| @ident | @string }
 
    Same as the previous one, except that the given ML terms will
@@ -328,6 +321,13 @@ what ML term corresponds to a given axiom.
       by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline`
       will have an effect on the realized and inlined axiom.
 
+   .. exn:: The term @qualid is already defined as foreign custom constant.
+
+      The :n:`@qualid` was previously used in a
+      :cmd:`Extract Foreign Constant` command. Using :cmd:`Extract Inlined Constant`
+      for :n:`@qualid` would override this command.
+
+
 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
 has no computational content and hence will not appear in extracted
@@ -469,7 +469,7 @@ OCaml code with C code, the linker needs to know
 
    .. exn:: Extract Foreign Constant is supported only for functions.
 
-      This error is thrown if :n:`@qualid` is of sort ``Type`` and external functions only
+      This error is thrown if :n:`@qualid` is of sort ``Type`` as external functions only
       work for functions.
 
    .. exn:: The term @qualid is already defined as inline custom constant.