Document "Print Debug GC" command and OCAMLRUNPARAM env variable

1 files changed, 15 insertions, 6 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 00aafe1266..4480b10319 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -858,19 +858,28 @@ Controlling the effect of proof editing commands
 Controlling memory usage
 ------------------------
 
+.. cmd:: Print Debug GC
+
+   Prints heap usage statistics, which are values from the `stat` type of the `Gc` module
+   described
+   `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_
+   in the OCaml documentation.
+   The `live_words`, `heap_words` and `top_heap_words` values give the basic information.
+   Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables.
+
 When experiencing high memory usage the following commands can be used
 to force |Coq| to optimize some of its internal data structures.
 
-
 .. cmd:: Optimize Proof
 
-   This command forces |Coq| to shrink the data structure used to represent
-   the ongoing proof.
+   Shrink the data structure used to represent the current proof.
 
 
 .. cmd:: Optimize Heap
 
-   This command forces the |OCaml| runtime to perform a heap compaction.
-   This is in general an expensive operation.
-   See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+   Perform a heap compaction.  This is generally an expensive operation.
+   See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
    There is also an analogous tactic :tacn:`optimize_heap`.
+
+Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>`
+environment variable.