diff options
| author | Pierre-Marie Pédrot | 2019-12-09 17:44:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-09 22:03:32 +0100 |
| commit | f00ad3178990c84c5169e4e86bb9a65dbfd539ff (patch) | |
| tree | ca23d27c85b8a8cefc4132ef1030aa3c85fb635a /library/libobject.ml | |
| parent | fa50ef6b47baa0d1c6ec79e6e4ec364fd47393a3 (diff) | |
Type-safe implementation of summary state.
For historical reasons we were wrapping the data stored in the summary objects
with dynamic type casts. There is no reason to do so since we have a proper
Dyn API. Furthermore, this had a small runtime cost when we knew that it was
never going to fail.
Diffstat (limited to 'library/libobject.ml')
0 files changed, 0 insertions, 0 deletions