diff options
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 6aaca9668..cac79625a 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -539,6 +539,9 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new more efficient and more general simplification algorithm on rings and semi-rings. +Laurent Théry and Bruno Barras developed a new significantly more efficient +simplification algorithm on fields. + Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and Claudio Sacerdoti Coen added new tactic features. @@ -567,8 +570,8 @@ Pierre Corbineau extended his tactic for solving first-order statements. He wrote a reflection-based intuitionistic tautology solver. -Pierre Courtieu and Julien Forest added extra support to reason on the -inductive structure of recursively defined functions. +Pierre Courtieu, Julien Forest and Yves Bertot added extra support to +reason on the inductive structure of recursively defined functions. Jean-Marc Notin significantly contributed to the general maintenance of the system. He also took care of {\textsf{coqdoc}}. @@ -576,6 +579,9 @@ of the system. He also took care of {\textsf{coqdoc}}. Pierre Castéran contributed to the documentation of (co-)inductive types and suggested improvements to the libraries. +Pierre Corbineau implemented a declarative mathematical proof +language, usable in combination with the tactic-based style of proof. + Finally, many users suggested improvements of the system through the Coq-Club mailing list and bug-tracker systems, especially user groups from INRIA Rocquencourt, Radbout University, University of |