diff options
| author | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
| commit | 424c1973e96dfbf3b2e3245d735853ffa9600373 (patch) | |
| tree | af087fa873c709e0066c8f6d81898f3aeae59b21 /doc/sphinx | |
| parent | 943fdd3277909f5229d95eb2e486944b0258648c (diff) | |
| parent | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (diff) | |
Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and #9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7b395900e9..afb0239be4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3912,6 +3912,8 @@ At Coq startup, only the core database is nonempty and can be used. environment, including those used for ``setoid_rewrite``, from the Classes directory. +:fset: internal database for the implementation of the ``FSets`` library. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. |