aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/coq_micromega.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-01 14:22:13 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-01 14:23:37 +0200
commit5ea872c80cc8b9d2845629cc75369f061e3bad05 (patch)
tree5c6183c776812e100a6694094ec9631e38fbc980 /plugins/micromega/coq_micromega.ml
parent5776f7d2b4753b89efa095a0f6774dac702fdfbd (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