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 /lib/cSet.mli | |
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 'lib/cSet.mli')
0 files changed, 0 insertions, 0 deletions