diff options
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 2f79e5f0..43216ed0 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -556,19 +556,19 @@ unresolved implicit has been implemented by Hugo Herbelin. Laurent Théry's contribution on strings and Pierre Letouzey and Jean-Christophe Filliâtre's contribution on finite maps have been integrated to the {\Coq} standard library. Pierre Letouzey developed a -library about finite sets ``à la Objective Caml'' and extended the -lists library. Pierre Letouzey's contribution on rational numbers -has been integrated too. +library about finite sets ``à la Objective Caml''. With Jean-Marc +Notin, he extended the library on lists. Pierre Letouzey's +contribution on rational numbers has been integrated and extended.. Pierre Corbineau extended his tactic for solving first-order -statements. He wrote a reflexion-based intuitionistic tautology +statements. He wrote a reflection-based intuitionistic tautology solver. -Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general -maintenance of the system. +Jean-Marc Notin significantly contributed to the general maintenance +of the system. He also took care of {\textsf{coqdoc}}. \begin{flushright} -Palaiseau, Apr. 2006\\ +Palaiseau, July 2006\\ Hugo Herbelin \end{flushright} @@ -577,7 +577,7 @@ Hugo Herbelin % Integration of ZArith lemmas from Sophia and Nijmegen. -% $Id: RefMan-pre.tex 8941 2006-06-09 16:43:42Z herbelin $ +% $Id: RefMan-pre.tex 9030 2006-07-07 15:37:23Z herbelin $ %%% Local Variables: %%% mode: latex |