From 7330ad2aafc4fe36abd4c51d18f1fe757a2cea2c Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Fri, 1 Sep 2017 16:12:47 -0400
Subject: add option index entry for NativeCompute Profiling

---
 doc/refman/RefMan-tac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6e27357008..8fbcfdf308 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
-- 
cgit v1.2.3