aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-03-22 11:24:27 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-06-13 10:30:29 +0200
commit295107103aaa86db8a31abb0e410123212648d45 (patch)
tree15928f2d0e3752e70938401555faddb48661f34d /.gitignore
parent423d3202fa0f244db36a0b1b45edfa61829201e6 (diff)
BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)
See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index e52091ee2..db12a9de2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -150,7 +150,6 @@ plugins/ssr/ssrvernac.ml
kernel/byterun/coq_jumptbl.h
kernel/copcodes.ml
tools/tolink.ml
-theories/Numbers/Natural/BigN/NMake_gen.v
ide/index_urls.txt
.lia.cache
checker/names.ml