From 94f1cb115b791a36ee660e94bf086e1638acbb88 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 14 Mar 2019 10:34:46 +0000
Subject: [Stdlib] OrderedType: do not pollute the “core” hint database

---
 doc/sphinx/proof-engine/tactics.rst | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fa6d62ffa2..85dfe0e5d2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3960,6 +3960,9 @@ At Coq startup, only the core database is nonempty and can be used.
 
 :fset: internal database for the implementation of the ``FSets`` library.
 
+:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module),
+               mainly used in the ``FSets`` and ``FMaps`` libraries.
+
 You are advised not to put your own hints in the core database, but
 use one or several databases specific to your development.
 
-- 
cgit v1.2.3