From 5737c8a41782ee66e96f4e855b00e396a23e8479 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 24 Oct 2016 17:39:06 +0200 Subject: Remove v62 from the refman. --- doc/refman/RefMan-tac.tex | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2da12c8d6..0aabaf6a8 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3493,8 +3493,7 @@ hints of the database named {\tt core}. \item {\tt auto with *} - Uses all existing hint databases, minus the special database - {\tt v62}. See Section~\ref{Hints-databases} + Uses all existing hint databases. See Section~\ref{Hints-databases} \item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ @@ -3962,8 +3961,8 @@ Several hint databases are defined in the \Coq\ standard library. The actual content of a database is the collection of the hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules potentially extend a -database. At {\Coq} startup, only the {\tt core} and {\tt v62} -databases are non empty and can be used. +database. At {\Coq} startup, only the {\tt core} database is non empty +and can be used. \begin{description} @@ -3998,18 +3997,8 @@ databases are non empty and can be used. from the \texttt{Classes} directory. \end{description} -There is also a special database called {\tt v62}. It collects all -hints that were declared in the versions of {\Coq} prior to version -6.2.4 when the databases {\tt core}, {\tt arith}, and so on were -introduced. The purpose of the database {\tt v62} is to ensure -compatibility with further versions of {\Coq} for developments done in -versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}). -The database {\tt v62} is intended not to be extended (!). It is not -included in the hint databases list used in the {\tt auto with *} tactic. - -Furthermore, you are advised not to put your own hints in the -{\tt core} database, but use one or several databases specific to your -development. +You are advised not to put your own hints in the {\tt core} database, +but use one or several databases specific to your development. \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ \mbox{\dots} \ident$_m$} -- cgit v1.2.3