diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -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 |