diff options
| author | Pierre-Marie Pédrot | 2018-11-03 16:27:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 16:27:59 +0100 |
| commit | 10e2f279d97b15939e6bdc7658dee20e09b06653 (patch) | |
| tree | e04f05e6ee1efe1abae01ccccb96ecc5e3646088 /dev/include | |
| parent | 228066a783a581ba2b304a12d9fe5e8decebcc48 (diff) | |
| parent | d6619dda80e30adb3d8699c896374657a32ca4e6 (diff) | |
Merge PR #8844: Move abstract out of tactics.ml
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions