diff options
| author | Théo Zimmermann | 2020-04-20 16:46:48 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-20 23:32:28 +0200 |
| commit | 0a38eb0630cab142f3d470e561ddb5090055068a (patch) | |
| tree | eff162fe677646218433387a2d9657938be76b4b /dev/ci/ci-basic-overlay.sh | |
| parent | 078e6c6d27bc3a13bb9e7ac6c9c5b8e05450af80 (diff) | |
[refman] Remove references to omega from Tactics chapter.
Omega was defined twice and this is the tactics chapter documentation
which was refered to from the tactic index. We remove it so that
users find the other reference (which contains the deprecation
notice).
The changes to the doc of zarith are a follow-up to #11976.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions