aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/vo.itarget
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2017-03-23 14:42:24 +0100
committerGravatar Matej Kosik <matej.kosik@inria.fr>2017-06-01 10:24:10 +0200
commit466e6a97c97e83679d49f0867d8f571402e1548f (patch)
treed51d462b1713dd00d216bb5095d8545e15962e8f /plugins/micromega/vo.itarget
parentf3a388baf9cf2a14a658cab77554a0802b999486 (diff)
extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/MExtraction.v"
Diffstat (limited to 'plugins/micromega/vo.itarget')
-rw-r--r--plugins/micromega/vo.itarget1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget
index c9009ea4d..a555d5ba1 100644
--- a/plugins/micromega/vo.itarget
+++ b/plugins/micromega/vo.itarget
@@ -1,3 +1,4 @@
+MExtraction.vo
EnvRing.vo
Env.vo
OrderedRing.vo