diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-01 14:34:17 +0200 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 14:37:04 +0200 |
| commit | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (patch) | |
| tree | f73623b8e154ed3251ab8ffe7a1c23888a9cbfe6 /library/global.ml | |
| parent | 2e8fb20e04da220cba68443a779c7ef6b08af9e5 (diff) | |
Patch from Enrico Tassi to get Drop compatible with stm.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions