diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-12 18:19:22 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:04 +0100 |
| commit | eb1eddf24932232890e32acf0fc4ff418ad0c281 (patch) | |
| tree | dfc7ee63bff57c21f28aacb7d57a634d35eacedd /library/global.ml | |
| parent | cee56f902fdae8a3de13ea93f0209f08ac256b08 (diff) | |
Dyn: add API to check of two Dyn.t are ==
A Dyn.t boxes a type tag with the original object, so calling
== on the Dyn.t does not work, hence this extra API.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions