diff --git a/Makefile b/Makefile
index 6c3ca5b55b668d803065baccb0727a23ea64344d..9ebb201d6da2e73a514ba47fc30b65219cc4e234 100644
--- a/Makefile
+++ b/Makefile
@@ -10,6 +10,12 @@ clean: Makefile.coq
 	+@make -f Makefile.coq clean
 	rm -f Makefile.coq
 
+uninstall:
+	+@make -f Makefile.uninstall uninstall
+
+install: Makefile.coq uninstall
+	+@make -f Makefile.coq install
+
 Makefile.coq: _CoqProject Makefile
 	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
 
@@ -19,4 +25,4 @@ Makefile: ;
 
 phony: ;
 
-.PHONY: all clean phony
+.PHONY: all clean install uninstall phony
diff --git a/Makefile.uninstall b/Makefile.uninstall
new file mode 100644
index 0000000000000000000000000000000000000000..3fb57d5aefd5eea558621cb8522751952d234361
--- /dev/null
+++ b/Makefile.uninstall
@@ -0,0 +1,27 @@
+## This makefile does some pretty heavy manipualtion of variables,
+## which we don't want in our main Makefile.  That's why it is
+## in a separate file.
+
+## BEGIN things copied from Makefile.coq
+# Here is a hack to make $(eval $(shell works:
+define donewline
+
+
+endef
+includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
+$(call includecmdwithout@,$(COQBIN)coqtop -config)
+
+ifdef USERINSTALL
+XDG_DATA_HOME?="$(HOME)/.local/share"
+COQLIBINSTALL=$(XDG_DATA_HOME)/coq
+COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
+else
+COQLIBINSTALL="${COQLIB}user-contrib"
+COQDOCINSTALL="${DOCDIR}user-contrib"
+COQTOPINSTALL="${COQLIB}toploop"
+endif
+
+## End things copied from Makefile.coq
+
+uninstall:
+	if [ -d "$(DSTROOT)"$(COQLIBINSTALL)/iris/ ]; then find "$(DSTROOT)"$(COQLIBINSTALL)/iris/ -name "*.vo" -print -delete; fi