diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-11 10:43:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-11 10:43:09 +0200 |
| commit | d4a8aa6339836b8ae1f37ae7ff67757009683542 (patch) | |
| tree | 400ac4f2cdff60125db92d69dbb176a79ded2043 /doc/refman | |
| parent | 545ec11e415b94b01980f8d4162939715f5b7ba1 (diff) | |
| parent | 7330ad2aafc4fe36abd4c51d18f1fe757a2cea2c (diff) | |
Merge PR #1014: Add option index entry for NativeCompute Profiling
Diffstat (limited to 'doc/refman')
| -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 |