diff options
| -rwxr-xr-x | doc/RefMan-pre.tex | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex index 6969ffd565..a60d98dca3 100755 --- a/doc/RefMan-pre.tex +++ b/doc/RefMan-pre.tex @@ -323,7 +323,6 @@ for type-checking terms. His approach was to use functional data-structures in order to get more sharing, to prepare the addition of modules and also to get closer to a certified kernel. - H. Herbelin introduced a new structure of terms with local definitions and redesigned the translation from the high-level language of Coq to the internal representation, in particular @@ -343,7 +342,12 @@ even involving universes and strong elimination. B. Barras improved the reduction strategy for lazy evaluation. Y. Bertot designed the \texttt{SearchPattern} and -\texttt{SearchRewrite} tools. +\texttt{SearchRewrite} tools and the support for the pcoq interface +(\url{http://www-sop.inria.fr/lemme/pcoq/}). + +C. Sacerdotti helped by H. Herbelin designed an XML output for the Coq +modules to be used in the Hypertextual Electronic Library of +Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}). A library for efficient representation of finite sets by binary trees contributed by J. Goubault was integrated in the basic theories.\\ |