aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vio_checking.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-01-12 14:24:01 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-01-12 14:24:01 +0100
commit1c6e7d3744d101124ed0152c2aac1e71c9f9d40d (patch)
treec3703906dfa0b1d3c43380afa477dd62859da916 /stm/vio_checking.mli
parente99e4006368fab3818812c6194d54465746c4566 (diff)
Update test for #3363 now that Require is forbidden inside modules.
Diffstat (limited to 'stm/vio_checking.mli')
0 files changed, 0 insertions, 0 deletions