diff options
author | 2015-01-23 14:22:53 +0100 | |
---|---|---|
committer | 2015-01-23 14:22:53 +0100 | |
commit | 87106cd6a0e613fc61943959d8fc7d3ff025fc5d (patch) | |
tree | 0bbcb291dc6cde03707e615024c6d3090186c8c2 /tactics/auto.ml | |
parent | c2d053c6f38a54e3083c8726eccb3e73942107b7 (diff) | |
parent | 4f632721be8b083126f49dd900a3294521879ec4 (diff) |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'tactics/auto.ml')
0 files changed, 0 insertions, 0 deletions