diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-18 16:10:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-18 18:29:29 +0100 |
| commit | 3f36f6fe68e1170f3d8c374e708513f05cc99619 (patch) | |
| tree | d19607582af6b66a79d325da132480ae766a6cce /checker/univ.ml | |
| parent | b49d803286ba9ed711313702bb4269c5e9c516fa (diff) | |
Cleaning up universe list implementation in Univ.
We use private types to ensure apriori hashconsing, and get rid of the
use of recursive modules. The hash of the universe list is also inlined
into each node instead of relying on a supplementary indirection.
Diffstat (limited to 'checker/univ.ml')
0 files changed, 0 insertions, 0 deletions