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 | |
| 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')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 |
2 files changed, 3 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. diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b58148ffff..b25104ddb9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -22,6 +22,7 @@ plugins/extraction/Extraction.v plugins/funind/FunInd.v plugins/funind/Recdef.v plugins/ltac/Ltac.v +plugins/micromega/DeclConstant.v plugins/micromega/Env.v plugins/micromega/EnvRing.v plugins/micromega/Fourier.v |