diff options
author | Paul Steckler <steck@stecksoft.com> | 2018-01-03 14:42:52 -0500 |
---|---|---|
committer | Paul Steckler <steck@stecksoft.com> | 2018-01-03 14:42:52 -0500 |
commit | c1960c794b5c8444925df67663bd70d35c67dc36 (patch) | |
tree | a34b777fb864a50291d5ca188630d743fe933e77 /doc | |
parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) |
add optimize_heap tactic for #6488
Diffstat (limited to 'doc')
-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 |