diff options
| author | Pierre-Marie Pédrot | 2019-10-04 17:59:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 17:59:20 +0200 |
| commit | d5f2e13e51c3404d326f04513a50d264790a7a4c (patch) | |
| tree | 7682460a0831a761fa61cc08b3e5adc324d2b585 /doc/sphinx/proof-engine | |
| parent | a8ab4cc9bfa9d31ac08b0ae3e3f318578ce50e2a (diff) | |
| parent | 94f1cb115b791a36ee660e94bf086e1638acbb88 (diff) | |
Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint database
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 3 |
1 files changed, 3 insertions, 0 deletions
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. |