aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-03 18:26:09 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-03 18:26:09 +0200
commitce6fbc60662042873d02479f7f2fb40601058a2a (patch)
tree2fcf494a7b12f75092bdb26efab793a9392d12a4 /tactics/tactics.ml
parent7525890df67fe711e2d3d63846ddb1e988d0812b (diff)
Test-suite for bug #2818.
Diffstat (limited to 'tactics/tactics.ml')
0 files changed, 0 insertions, 0 deletions