diff options
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index f8a9622c..2f79e5f0 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -536,8 +536,8 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new more efficient and more general simplification algorithm on rings and semi-rings. -Hugo Herbelin, Pierre Letouzey and Claudio Sacerdoti Coen added new -tactic features. +Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and +Claudio Sacerdoti Coen added new tactic features. Hugo Herbelin implemented matching on disjunctive patterns. @@ -547,7 +547,8 @@ connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc zenon}. Hugo Herbelin implemented an experimental protocol for calling external tools from the tactic language. -%Matthieu Sozeau developed an experimental language to reason over subtypes. +Matthieu Sozeau developed \textsc{Russell}, an experimental language +to specify the behavior of programs with subtypes. A mechanism to automatically use some specific tactic to solve unresolved implicit has been implemented by Hugo Herbelin. @@ -556,13 +557,15 @@ 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. +lists library. Pierre Letouzey's contribution on rational numbers +has been integrated too. Pierre Corbineau extended his tactic for solving first-order statements. He wrote a reflexion-based intuitionistic tautology solver. -Jean-Marc Notin took care of the general maintenance of the system. +Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general +maintenance of the system. \begin{flushright} Palaiseau, Apr. 2006\\ @@ -574,7 +577,7 @@ Hugo Herbelin % Integration of ZArith lemmas from Sophia and Nijmegen. -% $Id: RefMan-pre.tex 8707 2006-04-13 18:23:35Z herbelin $ +% $Id: RefMan-pre.tex 8941 2006-06-09 16:43:42Z herbelin $ %%% Local Variables: %%% mode: latex |