From 8a0986f84965e61239d00e9be48d713e60308863 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 28 Dec 2020 12:48:25 +0100 Subject: Document the -native-compiler option --- doc/sphinx/proofs/writing-proofs/rewriting.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'doc/sphinx/proofs') diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index b7f2927000..d271145af8 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 ` for details. .. flag:: NativeCompute Timing -- cgit v1.2.3