Reference Manual/Credits: native compute is a major contribution.

It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.

1 files changed, 5 insertions, 3 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e16002227..66f3369e3 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1011,12 +1011,14 @@ taking into account the universe levels of indices when computing the
 levels of inductive types. This supports using Coq as a tool to explore
 the relations between homotopy theory and type theory.
 
+Maxime Dénès and Benjamin Grégoire developed an implementation of
+conversion test and normal form computation using the OCaml native
+compiler. It complements the virtual machine conversion offering much
+faster computation for expensive functions.
+
 {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system.
 
-Maxime Dénès and Benjamin Grégoire developed an implementation of the
-conversion test using the OCaml native compiler.
-
 Maxime Dénès maintained the bytecode-based reduction machine.
 
 Pierre-Marie Pédrot has extended the syntax of terms to,