Reference manual: pass over the credit section for English.

1 files changed, 21 insertions, 20 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e75ade941..4af5c8fc6 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -939,9 +939,9 @@ projects:
 \begin{itemize}
 \item A new asynchronous evaluation and compilation mode by Enrico
   Tassi with help from Bruno Barras and Carst Tankink.
-\item The full integration of the new proof engine by Arnaud Spiwack
+\item Full integration of the new proof engine by Arnaud Spiwack
   helped by Pierre-Marie Pédrot,
-\item The addition of conversion and reduction based on native compilation
+\item Addition of conversion and reduction based on native compilation
   by Maxime Dénès and Benjamin Grégoire.
 \item Full universe polymorphism for definitions and inductive types by
   Matthieu Sozeau.
@@ -958,20 +958,21 @@ The way Coq processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
 proofs, the text between Proof and Qed, can be processed
 asynchronously, decoupling the checking of definitions and statements
-from the checking of proofs.  In interactive use, this improves the
-reactiveness of the system, since proofs can be processed in the
-background.  Similarly the compilation of a file can be split into two
-phases:  the first one checking only definitions and statements and
-the second one checking proofs.  A file resulting from the first
-phase, .vio extension, can be already Required.  All .vio files can be
-turned into complete .vo files in parallel.  The same infrastructure
-also allows terminating tactics to be run in parallel on a set of
-goals via the \verb=par:= goal selector.
-
-CoqIDE was modified to cope with asynchronous checking of the document.
-Its source code was also made separate from the one of Coq making it no
-more a special user interface and allowing its release cycle to be
-decoupled with the one of Coq.
+from the checking of proofs.  It improves the responsiveness of
+interactive development, since proofs can be processed in the
+background.  Similarly compilation of a file can be split into two
+phases: the first one checking only definitions and statements and the
+second one checking proofs.  A file resulting from the first
+phase~--~with the .vio extension~--~can be already Required.  All .vio
+files can be turned into complete .vo files in parallel.  The same
+infrastructure also allows terminating tactics to be run in parallel
+on a set of goals via the \verb=par:= goal selector.
+
+CoqIDE was modified to cope with asynchronous checking of the
+document.  Its source code was also made separate from that of Coq, so
+that CoqIDE no longer has a special status among user interfaces,
+paving the way for decoupling its release cycle from that of Coq in
+the future.
 
 Carst Tankink developed a Coq back end for user interfaces built on
 Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
@@ -982,13 +983,13 @@ funded by the Paral-ITP French ANR project.
 The full universe polymorphism extension was designed by Matthieu
 Sozeau. It conservatively extends the universes system and core calculus
 with definitions and inductive declarations parameterized by universes
-and constraints. It is based on a change of the kernel architecture to
+and constraints. It is based on a modification of the kernel architecture to
 handle constraint checking only, leaving the generation of constraints
 to the refinement/type inference engine. Accordingly, tactics are now
 fully universe aware, resulting in more localized error messages in case
 of inconsistencies and allowing higher-level algorithms like unification
 to be entirely type safe. The internal representation of universes has
-been modified but this invisible to the user. 
+been modified but this is invisible to the user. 
 
 The underlying logic has been extended with $\eta$-conversion for
 records defined with primitive projections by Matthieu Sozeau. This
@@ -999,11 +1000,11 @@ with typed equality. Primitive projections, which do not carry the
 parameters of the record and are rigid names (not defined as a
 pattern-matching construct), make working with nested records more
 manageable in terms of time and space consumption. This extension and
-universe polymorphism were carried partly while the author was working
+universe polymorphism were carried out partly while Matthieu Sozeau was working
 at the IAS in Princeton.
 
 The guard condition has been made compliant with extensional equality
-principles such as propositional equality and univalence, thanks to
+principles such as propositional extensionality and univalence, thanks to
 Maxime Dénès and Bruno Barras. To ensure compatibility with the
 univalence axiom, a new flag ``-indices-matter'' has been implemented, 
 taking into account the universe levels of indices when computing the