diff options
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 10 | ||||
-rw-r--r-- | doc/refman/RefMan-pro.tex | 8 |
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 |