diff options
| author | Pierre-Marie Pédrot | 2019-07-23 12:29:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-23 12:49:26 +0200 |
| commit | 0d2a8cb6cac3172fffe47703a811e9d8f288d0ed (patch) | |
| tree | c4f1427306c7d45203fd21cd0f9e7ea5dd2d89e4 /doc/stdlib | |
| parent | ae82afbaebb7f3a328498d4cc541d299423a7637 (diff) | |
Do not rely on dummy TACTIC EXTEND for ssreflect tactics.
We register the ML tactics by hand using the low-level API.
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions