diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-12 10:31:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-17 01:17:54 +0100 |
| commit | be7f6f003ff4318dbe962ec141060a9daf92a80d (patch) | |
| tree | 90b7617677f0b07a714215535a57b62377aaf4db /lib/loc.ml | |
| parent | 32a18b19f99c82dea5358bdebeb19862d30c4973 (diff) | |
Reimplementing Genarg safely.
No more Obj.magic in Genarg. We leverage the expressivity of GADT
coupled with dynamic tags to get rid of unsafety. For now the API
did not change in order to port the legacy code more easily.
Diffstat (limited to 'lib/loc.ml')
0 files changed, 0 insertions, 0 deletions