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

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