diff options
| author | Théo Zimmermann | 2019-05-07 14:27:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-08 21:27:46 +0200 |
| commit | d3a33d5d5177d301d0fbae08fde7e82be2bf3351 (patch) | |
| tree | 0373e6426ca88a81b02058e2336910a0da461eb3 /dev/doc/debugging.md | |
| parent | 86fd245bfd5c9750b515ea4204b0a9a50c14d930 (diff) | |
[refman] Move all the Ltac examples to the Ltac chapter.
The Detailed examples of tactics chapter can be removed when the
remaining examples are moved closer to the definitions of the
corresponding tactics.
This commit also moves back the footnotes from the Tactics chapter at
the end of the chapter, and removes an old footnote that doesn't
matter anymore.
Diffstat (limited to 'dev/doc/debugging.md')
0 files changed, 0 insertions, 0 deletions