aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/workerPool.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-12-05 07:27:06 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-23 21:58:36 +0100
commit80d36bc6538b7feaab3dfa43f6e234ae85b55692 (patch)
treed3a36cc8dcaf0542194c9d672396dcad80131b04 /stm/workerPool.ml
parent67f7e1103ffb5dae052595e4db00e0214e54474d (diff)
A test checking for non-collision of name in irrefutable patterns.
Diffstat (limited to 'stm/workerPool.ml')
0 files changed, 0 insertions, 0 deletions