diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-01 14:22:13 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-01 14:23:37 +0200 |
commit | 5ea872c80cc8b9d2845629cc75369f061e3bad05 (patch) | |
tree | 5c6183c776812e100a6694094ec9631e38fbc980 /plugins/micromega/coq_micromega.ml | |
parent | 5776f7d2b4753b89efa095a0f6774dac702fdfbd (diff) |
More efficient data structure to check if a native file is loaded.
Spotted by PMP.
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
0 files changed, 0 insertions, 0 deletions