From b855224b5ce5deda9853af1bed9b135a7ea9a76b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 10:01:49 +0100
Subject: 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.---
 doc/refman/RefMan-pre.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e160022279..66f3369e3b 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,
-- 
cgit v1.2.3