diff options
| author | mohring | 2001-04-19 11:12:21 +0000 |
|---|---|---|
| committer | mohring | 2001-04-19 11:12:21 +0000 |
| commit | 31dd386cbd48502033ab5ff3503d73c9ddb6fda3 (patch) | |
| tree | ee930f5cfa7e7d8faeac680e29b16ffc68a88245 | |
| parent | a87d329217a38a7334579767bd983e5225f0e0a7 (diff) | |
Mise a jour credits V7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8190 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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.\\ |