diff options
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -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 |