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/changelog/10-standard-library/09772-ordered_type-hint-db.rst | 4 ++++ doc/sphinx/proof-engine/tactics.rst | 3 +++ 2 files changed, 7 insertions(+) create mode 100644 doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst new file mode 100644 index 0000000000..7babcdb6f1 --- /dev/null +++ b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst @@ -0,0 +1,4 @@ +- Moved the `auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 `_, + by Vincent Laporte). 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