diff options
author | 2015-04-10 16:14:09 +0200 | |
---|---|---|
committer | 2015-04-10 16:14:09 +0200 | |
commit | 07d63e1333dc73eda3e49e904ff8df6e7f62fa79 (patch) | |
tree | fad7851b41d628895b717d8915ae9c1a7d5f271a /tactics/tactics.ml | |
parent | 9cd8bbc7808479c71e4413bc6f3555f494feda09 (diff) |
Test for bug #3199.
Diffstat (limited to 'tactics/tactics.ml')
0 files changed, 0 insertions, 0 deletions