diff options
author | Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
commit | de0085539583f59dc7c4bf4e272e18711d565466 (patch) | |
tree | 347e1d95a2df56f79a01b303e485563588179e91 /doc/refman/RefMan-pre.tex | |
parent | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff) |
Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2
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 |