diff options
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 41bb0a566..7159fc0b2 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -863,7 +863,7 @@ to analyze the structure of type universes. Regarding libraries, a new library about lists of a given length (called vectors) has been provided by Pierre Boutillier. -Pierre Corbineau maintained the C-zar proof mode. +Pierre Corbineau maintained the C-zar proof mode. Bruno Barras and Benjamin Gr\'egoire maintained the call-by-value reduction machines. @@ -903,8 +903,9 @@ benchmarking support was provided by Jean-Marc Notin. Many suggestions for improvements were motivated by feedback from users, on either the bug tracker or the coq-club mailing list. Special thanks are going to the users who contributed patches, starting with -Tom Prince. Other patch contributors include C\'edric Auger, David Baelde, -Dan Grayson and Marc Lasson. +Tom Prince. Other patch contributors include C\'edric Auger, David +Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, +Hendrik Tews and Eelis van der Weegen. \begin{flushright} Paris, December 2011\\ |