diff --git a/.gitignore b/.gitignore
index a92e6ebdf857302d2fbf70dab1be2fec9082412d..7b752f404eb0cb26a7a27d9af0cd20e0efe3543b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,32 +1,8 @@
 *.vo
+*.v.d
 *.glob
-.sconsign.dblite
-deps
-old/*
-coqidescript
-\#*\#
-*.pyc
-*~
-*.cmi
-*.cmx
-*.cmo
-*.o
-utils/coq2html
-utils/coq2html.ml
-doc/ch2o.*.html
 *.cache
-*.broken
-broken/*
-*.patch
-parser/Extracted.*
-parser/Lexer.ml
-parser/Parser.ml
-parser/Parser.mli
-parser/Include.*
-_build/
-ch2o
-*.native
-*.byte
-a.out
 *.aux
+\#*\#
+*~
 .coq-native/
diff --git a/SConstruct b/SConstruct
deleted file mode 100644
index b55ee77e3b3cb4e3543e87aa37af27e8649ef7ab..0000000000000000000000000000000000000000
--- a/SConstruct
+++ /dev/null
@@ -1,15 +0,0 @@
-# Copyright (c) 2012-2015, Robbert Krebbers.
-# This file is distributed under the terms of the BSD license.
-import os, glob, string
-
-modules = ["prelude", "modures", "iris", "barrier"]
-Rs = '-Q . ""'
-env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
-
-# Coq dependencies
-vs = [x for m in modules for x in glob.glob(m + '/*.v')]
-if os.system('coqdep ' + Rs + ' ' + ' '.join(map(str, vs)) + ' > deps'): Exit(2)
-ParseDepends('deps')
-
-# Coq files
-for v in vs: env.Coq(v)
diff --git a/site_scons/site_tools/Coq.py b/site_scons/site_tools/Coq.py
deleted file mode 100644
index ae02408221d29e40ef2280ec26599efd1e9cf6c2..0000000000000000000000000000000000000000
--- a/site_scons/site_tools/Coq.py
+++ /dev/null
@@ -1,21 +0,0 @@
-# Copyright (c) 2012-2015, Robbert Krebbers.
-# This file is distributed under the terms of the BSD license.
-import SCons.Defaults, SCons.Tool, SCons.Util, os
-
-def coq_emitter(target, source, env):
-  base, _ = os.path.splitext(str(target[0]))
-  target.append(base + ".glob")
-  return target, source
-Coq = SCons.Builder.Builder(
-  action = '$COQC $COQFLAGS -q $SOURCE',
-  suffix = '.vo',
-  src_suffix = '.v',
-  emitter = coq_emitter
-)
-
-def generate(env):
-  env['COQC'] = 'coqc'
-  env.Append(BUILDERS = { 'Coq' : Coq })
-
-def exists(env):
-  return env.Detect('coqc')