Apply suggestions from code review

Accepting change proposals given by @jfehrle

Co-authored-by: Jim Fehrle <[email protected]>

doc/sphinx/addendum/extraction.rst

@@ -402,38 +402,37 @@ As an example of translation to a non-inductive datatype, let's turn
 Generating FFI Code
 ~~~~~~~~~~~~~~~~~~~
 
-The plugin provides mechanisms to generate (currently only) OCaml code to
+The plugin provides mechanisms to generate only OCaml code to
 interface the generated OCaml code with C programs. In order to link compiled
 OCaml code with C code, the linker needs to know
 
- * which C functions will be called by the ML code (external)
- * which ML functions shall be accessible by the C code (callbacks)
+   * which C functions will be called by the ML code (external)
+   * which ML functions shall be accessible by the C code (callbacks)
 
 .. cmd:: Extract Foreign Constant @qualid => @string
 
-   Same as the :cmd:`Extract Constant`, except that the given ML terms
+   Like :cmd:`Extract Constant`, except that the referenced ML terms
    will be declared in the form
 
    ``external @qualid : ML type = "@string"``.
 
 .. caution::
 
-   * The external function name provided by the user as :n:`@string`
-     is currently **not** checked at all by extraction, even for syntax errors.
+   * The external function name :n:`@string` is not checked in any way.
 
-   * It is the responsibility of the user to ensure that the C
-     functions given to realize the axioms do have the expected or compatible
+   * The user must ensure that the C
+     functions given to realize the axioms have the expected or compatible
      types. In fact, the strings containing realizing code are just copied to the
      extracted files.
 
 .. exn:: Extract Foreign Constant is supported only for OCaml extraction
 
-   We currently only support calling foreign functions for OCaml.
+   Foreign function calls are only supported for OCaml.
 
 .. exn:: The term @qualid is already defined as custom constant.
 
-   This error message means that the :n:`@qualid` was previously used in the command
-   :cmd:`Extract Constant` or :cmd:`Extract Inlined Constant`. Using :cmd:`Extract Foreign Constant`
+   The :n:`@qualid` was previously used in a
+   :cmd:`Extract Constant` or :cmd:`Extract Inlined Constant` command. Using :cmd:`Extract Foreign Constant`
    for :n:`@qualid` would override those commands.
 
 .. cmd:: Extract Callback {? @string } @qualid
@@ -448,45 +447,43 @@ OCaml code with C code, the linker needs to know
    If no alias is specified, it is set to the string representation of :n:`@qualid`.
 
 .. caution::
-   * The optional alias provided by the user as :n:`@string`
-     is currently **not** checked at all by extraction, even for syntax errors.
+   * The optional alias :n:`@string` is currently **not** checked in any way.
 
-   * It is the responsibility of the user to ensure that the callback aliases are
+   * The user must ensure that the callback aliases are
      unique, i.e. when multiple modules expose a callback, the user should make
      sure that no two :n:`@qualid` share the same alias.
 
 .. note::
    Using Extract Callback has no impact on the rest of the synthesised code since
-   it is an additional declaration. Thus, there is also no impact on correctness
+   it is an additional declaration. Thus, there is no impact on the correctness
    and type safety of the generated code.
 
 .. exn:: Extract Callback is supported only for OCaml extraction
 
-   The concept of callback registration via calling ``Callback.register`` is specific
-   for OCaml. Thus, the command is only usable when extracting OCaml code.
+   The callback registration mechanism ``Callback.register`` is specific
+   to OCaml. Thus, the command is only usable when extracting OCaml code.
 
 .. cmd:: Print Extraction Foreign
 
-   Prints the current state of the set recording the custom foreigns
-   declared by the command :cmd:`Extract Foreign Constant` together with
-   the defined foreign ML function name.
+   Prints the current set of custom foreign functions
+   declared by the command :cmd:`Extract Foreign Constant` together with its
+   associated foreign ML function name.
 
 .. cmd:: Reset Extraction Foreign
 
-   Resets the current state of the set recording the custom externals
+   Resets the set of custom externals
    declared by the command :cmd:`Extract Foreign Constant`.
 
 .. cmd:: Print Extraction Callback
 
-   Prints the current state of the map recording the callbacks
-   declared by the command :cmd:`Extract Callback`
-   by printing the respective :token:`qualid` and callback alias
-   :token:`string` or "no custom alias" if the optional :token:`string`
-   was not set for that :token:`qualid`.
+   Prints the map of callbacks
+   declared by the command :cmd:`Extract Callback`,
+   showing the :token:`qualid` and callback alias
+   :token:`string` (if specified) for each callback.
 
 .. cmd:: Reset Extraction Callback
 
-   Resets the current state of the map recording the callbacks
+   Resets the the map recording the callbacks
    declared by the command :cmd:`Extract Callback`.