aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-23 15:59:03 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-23 15:59:03 +0200
commite2b64c6df6e59dda27b3b19ca8bde19c2bdf35e2 (patch)
tree3b5dd3d9e6d487ef69f8136884b6b07cf98f12ed /tactics/tacticals.ml
parentdb37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 (diff)
Oops, I fixed the .ml's
Diffstat (limited to 'tactics/tacticals.ml')
0 files changed, 0 insertions, 0 deletions