diff options
author | Matej Kosik <matej.kosik@inria.fr> | 2017-03-23 14:42:24 +0100 |
---|---|---|
committer | Matej Kosik <matej.kosik@inria.fr> | 2017-06-01 10:24:10 +0200 |
commit | 466e6a97c97e83679d49f0867d8f571402e1548f (patch) | |
tree | d51d462b1713dd00d216bb5095d8545e15962e8f /.gitignore | |
parent | f3a388baf9cf2a14a658cab77554a0802b999486 (diff) |
extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/MExtraction.v"
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 98d974197..84b9844a5 100644 --- a/.gitignore +++ b/.gitignore @@ -175,3 +175,7 @@ user-contrib .*.sw* test-suite/.lia.cache test-suite/.nra.cache + +# these files are generated from plugins/micromega/MExtraction.v +plugins/micromega/micromega.ml +plugins/micromega/micromega.mli |