Merge PR #6497: Add optimize_heap tactic for #6488

2 files changed, 14 insertions, 4 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index ef0f4af8f..c4c0435c5 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1426,6 +1426,16 @@ You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, whi
 
 Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
 
+\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}.
+
+The following tactic behaves like {\tt idtac}, and running it compacts the heap in the
+OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}).
+
+\tacindex{optimize\_heap}
+\begin{quote}
+{\tt optimize\_heap}.
+\end{quote}
+
 \endinput
 
 \subsection{Permutation on closed lists}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 1d3311edc..3d4c885b3 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -555,12 +555,12 @@ used to force Coq to optimize some of its internal data structures.
 This command forces Coq to shrink the data structure used to represent
 the ongoing proof.
 
-\subsection[\tt Optimize Heap.]{\tt Optimize Heap.}
+\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}}
 
 This command forces the OCaml runtime to perform a heap compaction.
-This is in general an expensive operation.  See:
-  \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact}
-
+This is in general an expensive operation.  See: \\
+\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\
+There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}).
 
 %%% Local Variables: 
 %%% mode: latex