diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..81e7db3db80242e5a807acef2dfc4cd59ff54b29
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,13 @@
+*.vo
+*.vio
+*.v.d
+*.glob
+*.cache
+*.aux
+\#*\#
+.\#*
+*~
+*.bak
+.coq-native/
+Makefile.coq
+*.crashcoqide
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000000000000000000000000000000000000..0b9458c293683d7b6b651b0c7ea6e9da42c4a5af
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+All files in this development are distributed under the terms of the BSD
+license, included below.
+
+------------------------------------------------------------------------------
+
+ BSD LICENCE
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+ * Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+ * Neither the name of the <organization> nor the
+ names of its contributors may be used to endorse or promote products
+ derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..db003e171542c0f9a8b32562fb44b2226a42aee1
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,46 @@
+# Process flags
+ifeq ($(Y), 1)
+ YFLAG=-y
+endif
+
+# Determine Coq version
+COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
+COQ_MAKEFILE_FLAGS ?=
+
+ifeq ($(COQ_VERSION), 8.6)
+ COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+endif
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+ +@make -f Makefile.coq $@
+
+all: Makefile.coq
+ +@make -f Makefile.coq all
+
+clean: Makefile.coq
+ +@make -f Makefile.coq clean
+ find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+ rm -f Makefile.coq
+
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
+Makefile.coq: _CoqProject Makefile awk.Makefile
+ coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
+ mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
+
+# Install build-dependencies
+build-dep:
+ build/opam-pins.sh < opam.pins
+ opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
+ opam pin add coq-prelude "$$(pwd)#HEAD" -k git -n -y
+ opam install coq-prelude --deps-only $(YFLAG)
+ opam pin remove coq-prelude
+
+# Some files that do *not* need to be forwarded to Makefile.coq
+Makefile: ;
+_CoqProject: ;
+awk.Makefile: ;
+
+# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
+phony: ;
+.PHONY: all clean phony
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..a7869b1351ef752e6797dcbc94d5d18a0f6c1e7f
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,40 @@
+-Q theories stdpp
+theories/option.v
+theories/fin_map_dom.v
+theories/bset.v
+theories/fin_maps.v
+theories/vector.v
+theories/pmap.v
+theories/stringmap.v
+theories/fin_collections.v
+theories/mapset.v
+theories/proof_irrel.v
+theories/hashset.v
+theories/pretty.v
+theories/countable.v
+theories/orders.v
+theories/natmap.v
+theories/strings.v
+theories/relations.v
+theories/collections.v
+theories/listset.v
+theories/streams.v
+theories/gmap.v
+theories/gmultiset.v
+theories/base.v
+theories/tactics.v
+theories/prelude.v
+theories/listset_nodup.v
+theories/finite.v
+theories/numbers.v
+theories/nmap.v
+theories/zmap.v
+theories/coPset.v
+theories/lexico.v
+theories/set.v
+theories/decidable.v
+theories/list.v
+theories/functions.v
+theories/hlist.v
+theories/sorting.v
+
diff --git a/awk.Makefile b/awk.Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..09ded0aa64f3a85ee4a55668d21ee17bb9a362f0
--- /dev/null
+++ b/awk.Makefile
@@ -0,0 +1,35 @@
+# awk program that patches the Makefile generated by Coq.
+
+# Detect the name this project will be installed under.
+/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
+# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
+# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
+# we can just split the string at '/' here.
+ split($0, PIECES, /\//);
+ PROJECT=PIECES[2];
+}
+
+# Patch the uninstall target to work properly, and to also uninstall stale files.
+# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
+/^uninstall:/ {
+ print "uninstall:";
+ print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
+ getline;
+ next
+}
+
+# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring
+# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
+# files where the .vo is *older* than the .vio.
+/^vio2vo:/ {
+ print "vio2vo:";
+ print "\t@make -j $(J) quick"
+ print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\"
+ print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
+ print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
+ getline;
+ next
+}
+
+# This forwards all unchanged lines
+1