diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-14 15:43:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:33 +0200 |
| commit | 3c6679676c3963b7c3ec7c1eadbf24ae70311408 (patch) | |
| tree | 1de23a7b0802e899d2bf3d8f189f31f7f8e0f745 /library/global.ml | |
| parent | 9961577dfbb93f0b691c355ba99822665def037f (diff) | |
More precise type of entries capturing their lack of side-effects.
We sprinkle a few GADTs in the kernel in order to statically ensure that
entries are pure, so that we get stronger invariants.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions