diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-21 20:10:26 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-23 12:50:45 +0100 |
commit | f4ee7ee31e4bc4a49de784d90b331abd3a21e34f (patch) | |
tree | ce42b1cbd9045d2f5b67435d1bd59fbba389b85b /pretyping/pretyping.ml | |
parent | 865c8cd9c3d6cd5dd91a86a26b81efe53bdf444a (diff) |
Fixing 934761875 about optimizing Import of several libraries at once (thanks to Enrico for noticing a bug).
Diffstat (limited to 'pretyping/pretyping.ml')
0 files changed, 0 insertions, 0 deletions