diff options
| author | Théo Zimmermann | 2020-07-13 15:09:25 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-07-13 15:09:25 +0200 |
| commit | f238b252019555c0a9ae5bb0f56b4c73192b1e86 (patch) | |
| tree | 722f93abd2f359bc51ea616cfa514558644430dc /dev | |
| parent | f4593ab277c12eda7e000011eeb2276716ac9a09 (diff) | |
| parent | f91f2ac64fbc7035c77592195c67050640abc3cb (diff) | |
Merge PR #12681: tactics.rst: `Require A` is enough for `A`'s hints
Reviewed-by: Zimmi48
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions