aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cSet.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-12 18:19:22 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 15:05:04 +0100
commiteb1eddf24932232890e32acf0fc4ff418ad0c281 (patch)
treedfc7ee63bff57c21f28aacb7d57a634d35eacedd /lib/cSet.mli
parentcee56f902fdae8a3de13ea93f0209f08ac256b08 (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