diff options
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore index f0dd91db9..98479902a 100644 --- a/.gitignore +++ b/.gitignore @@ -106,7 +106,6 @@ ide/config_parser.mli lib/pp.ml lib/compat.ml -lib/refutpat.ml parsing/g_xml.ml parsing/g_prim.ml parsing/q_util.ml @@ -141,7 +140,6 @@ plugins/funind/g_indfun.ml plugins/omega/g_omega.ml plugins/quote/g_quote.ml plugins/groebner/groebner.ml -plugins/groebner/ideal.ml plugins/micromega/g_micromega.ml plugins/subtac/g_subtac.ml plugins/fourier/g_fourier.ml |