diff options
| author | coqbot-app[bot] | 2020-12-30 07:10:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-30 07:10:06 +0000 |
| commit | 30f648dc29958add42e7509a9c29f271f768e183 (patch) | |
| tree | 5dccaadf3ccf8f48481811336d8f3ae9bee43222 /doc/sphinx/proofs | |
| parent | 810e91530071159e27e89bf0ca6bc36c8bb1d034 (diff) | |
| parent | 8a0986f84965e61239d00e9be48d713e60308863 (diff) | |
Merge PR #13684: Document the -native-compiler option
Reviewed-by: silene
Ack-by: Zimmi48
Ack-by: jfehrle
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 |