diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 3649202b45..90404b7321 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -442,7 +442,10 @@ the conversion in hypotheses :n:`{+ @ident}`. in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive - computations. + computations. Depending on the configuration, this tactic can either default to + :tacn:`vm_compute`, recompile dependencies or fail due to some missing + precompiled dependencies, + see :ref:`the native-compiler option <native-compiler-options>` for details. .. flag:: NativeCompute Timing |