diff options
author | 2010-07-08 18:10:54 +0000 | |
---|---|---|
committer | 2010-07-08 18:10:54 +0000 | |
commit | a7073580104d2e51ffb446b133b5846d9f14e49e (patch) | |
tree | b49009c6fddfb97cea69ec6a4402a9304c2106a5 | |
parent | 44e80ba4e4c863e0c38cc7cf6a65579640385436 (diff) |
Updating reference manual credits: gb is now nsatz.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/refman/RefMan-pre.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 8ec3c2e7f..c45944ce0 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -695,7 +695,7 @@ Hugo Herbelin\\ {\Coq} version 8.3 is before all a transition version with refinements or extensions of the existing features and libraries and a new tactic -{\tt gb} based on Hilbert's Nullstellensatz for deciding systems of +{\tt nsatz} based on Hilbert's Nullstellensatz for deciding systems of equations over rings. With respect to libraries, the main evolutions are due to Pierre @@ -726,10 +726,10 @@ convenient operator \verb!<+! for nesting functor application, what provides a light notation for inheriting the properties of cascading modules. -The new tactic {\tt gb} is due to Loïc Pottier. It works by computing -Gr\"obner bases what explains its name. Regarding the existing -tactics, various improvements have been done by Matthieu Sozeau, Hugo -Herbelin and Pierre Letouzey. +The new tactic {\tt nsatz} is due to Loïc Pottier. It works by +computing Gr\"obner bases. Regarding the existing tactics, various +improvements have been done by Matthieu Sozeau, Hugo Herbelin and +Pierre Letouzey. Matthieu Sozeau extended and refined the type classes and {\tt Program} features (the {\sc Russell} language). Pierre Letouzey |