diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-09-01 16:12:47 -0400 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-09-01 16:12:47 -0400 |
| commit | 7330ad2aafc4fe36abd4c51d18f1fe757a2cea2c (patch) | |
| tree | 5fb4d8e07b355be31a7d1feadaa5fbf56fa6d91d /doc | |
| parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
add option index entry for NativeCompute Profiling
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6e2735700..8fbcfdf30 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3309,7 +3309,7 @@ evaluating purely computational expressions (i.e. with little dead code). fine-tuned. It is specially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. -\item {\tt native\_compute} \tacindex{native\_compute} +\item {\tt native\_compute} \tacindex{native\_compute} \optindex{NativeCompute Profiling} This tactic evaluates the goal by compilation to \ocaml{} as described in \cite{FullReduction}. If \Coq{} is running in native code, it can be typically |