diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-23 19:59:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-23 19:59:42 +0000 |
| commit | ed45105a4601addccd1d7920d8ad9b5999eddf30 (patch) | |
| tree | 8d2900eae3c11023c6ca5219fc06d3a9a8dbdaa9 /doc/refman | |
| parent | ed2ffef62c76f3b716b1be0fab8adca507cd5c58 (diff) | |
Credits for 8.4: More exhaustive list of external contributors.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -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\\ |