Merge pull request #32250 from vbgl/coq-clean

coq_HEAD, coqPackages_8_4: remove

19 files changed, 6 insertions, 1666 deletions

diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix
deleted file mode 100644
index 968ea74e2960..000000000000
--- a/pkgs/applications/science/logic/coq/HEAD.nix
+++ /dev/null
@@ -1,81 +0,0 @@
-# - coqide compilation can be disabled by setting buildIde to false;
-# - The csdp program used for the Micromega tactic is statically referenced.
-#   However, coq can build without csdp by setting it to null.
-#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
-
-{stdenv, fetchgit, writeText, pkgconfig, ocamlPackages_4_02, ncurses, buildIde ? true, csdp ? null}:
-
-let
-  version = "2017-02-03";
-  coq-version = "8.6";
-  ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages_4_02.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
-  csdpPatch = if csdp != null then ''
-    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
-    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
-  '' else "";
-  ocaml = ocamlPackages_4_02.ocaml;
-  findlib = ocamlPackages_4_02.findlib;
-  lablgtk = ocamlPackages_4_02.lablgtk;
-  camlp5 = ocamlPackages_4_02.camlp5_transitional;
-in
-
-stdenv.mkDerivation {
-  name = "coq-unstable-${version}";
-
-  inherit coq-version;
-  inherit ocaml camlp5 findlib;
-
-  src = fetchgit {
-    url = git://scm.gforge.inria.fr/coq/coq.git;
-    rev = "078598d029792a3d9a54fae9b9ac189b75bc3b06";
-    sha256 = "0sflrpp6x0ada0bjh67q1x65g88d179n3cawpwkp1pm4kw76g8x7";
-  };
-
-  nativeBuildInputs = [ pkgconfig ];
-  buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ];
-
-  postPatch = ''
-    UNAME=$(type -tp uname)
-    RM=$(type -tp rm)
-    substituteInPlace configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
-    substituteInPlace configure.ml --replace "\"Darwin\"; \"FreeBSD\"; \"OpenBSD\"" "\"Darwinx\"; \"FreeBSD\"; \"OpenBSD\""
-    ${csdpPatch}
-  '';
-
-  setupHook = writeText "setupHook.sh" ''
-    addCoqPath () {
-      if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then
-        export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
-      fi
-    }
-
-    envHooks=(''${envHooks[@]} addCoqPath)
-  '';
-
-  preConfigure = ''
-    configureFlagsArray=(
-      -opt
-      ${ideFlags}
-    )
-  '';
-
-  prefixKey = "-prefix ";
-
-  buildFlags = "revision coq coqide";
-
-  meta = with stdenv.lib; {
-    description = "Coq proof assistant";
-    longDescription = ''
-      Coq is a formal proof management system.  It provides a formal language
-      to write mathematical definitions, executable algorithms and theorems
-      together with an environment for semi-interactive development of
-      machine-checked proofs.
-    '';
-    homepage = http://coq.inria.fr;
-    license = licenses.lgpl21;
-    branch = coq-version;
-    maintainers = with maintainers; [ roconnor thoughtpolice vbgl ];
-    platforms = platforms.unix;
-  };
-}
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index af7ef8001d39..a65dad546617 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -2,12 +2,6 @@
 
 let param =
   {
-    "8.4" = {
-      version = "20160529";
-      rev = "a9e89f1d4246a787bf1d8873072077a319635c3e";
-      sha256 = "14ng71p890q12xvsj00si2a3fjcbsap2gy0r8sxpw4zndnlq74wa";
-    };
-
     "8.5" = {
       version = "20170512";
       rev = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03";
diff --git a/pkgs/development/coq-modules/bedrock/default.nix b/pkgs/development/coq-modules/bedrock/default.nix
deleted file mode 100644
index fc3c16d00492..000000000000
--- a/pkgs/development/coq-modules/bedrock/default.nix
+++ /dev/null
@@ -1,39 +0,0 @@
-{stdenv, fetchurl, coq}:
-
-stdenv.mkDerivation rec {
-
-  name = "coq-bedrock-${coq.coq-version}-${version}";
-  version = "20140722";
-
-  src = fetchurl {
-    url = "http://plv.csail.mit.edu/bedrock/bedrock-${version}.tgz";
-    sha256 = "0aaa98q42rsy9hpsxji21bqznizfvf6fplsw6jq42h06j0049k80";
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  enableParallelBuilding = true;
-
-  buildPhase = ''
-    make -j$NIX_BUILD_CORES -C src/reification
-    make -j$NIX_BUILD_CORES -C src
-    make -j$NIX_BUILD_CORES -C src native
-    # make -j$NIX_BUILD_CORES -C platform
-    # make -j$NIX_BUILD_CORES -C platform -f Makefile.cito
-  '';
-
-  installPhase = ''
-    COQLIB=$out/lib/coq/${coq.coq-version}/
-    mkdir -p $COQLIB/user-contrib/Bedrock
-    cp -pR src/* $COQLIB/user-contrib/Bedrock
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = http://plv.csail.mit.edu/bedrock/;
-    description = "A library that turns Coq into a tool much like classical verification systems";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/development/coq-modules/contribs/all.nix b/pkgs/development/coq-modules/contribs/all.nix
deleted file mode 100644
index d2ef82c55875..000000000000
--- a/pkgs/development/coq-modules/contribs/all.nix
+++ /dev/null
@@ -1,163 +0,0 @@
-{
-AACTactics = "0v18kf7xjys4g3z8m2sfiyipyn6mz75wxl2zgqk7nv1jr8i03min";
-ABP = "06cn70lbdivn1hxnlsqpiibq9nlwl6dggcn967q6n3nph37m4pdp";
-AILS = "1g0hc27kizrwm6x35j3w721cllfl4rvhiqifn3ljy868mwxwsiva";
-AMM11262 = "15rxr5bzyswxfznml4vij3pflqm3v2bl1xzg9m1p5gmd0385zh6l";
-ATBR = "1xfhc70m9qm51gwi7cls8znx37y5cp1m0wak1h0r51g1d2lxr7a6";
-Additions = "0bhl1wqbqigq0m6zj1yhdm5j0rsn75xy510kz9qy4dv5277wc7ab";
-Algebra = "061szlbg5zh5h0ksgmw34hqrvqy6794p3r1ijg0xi8mqa2wpbjd8";
-Angles = "1grqx88mibz4lg7k9ba89vpg4kwrm3s87wy0ls39i3d3wgx18n97";
-AreaMethod = "07d86p5xbnhbrily18hda0hymf3zx8yhw905plmrqyfbcc6x5531";
-Automata = "0g75gjdj79ysiq1pwqk658jxs2z1l8pk702iz69008vkjzbzkhvm";
-AxiomaticABP = "19x16dgsqyw2pflza8cgv29585a6yy3r8pz4z8ns3r7qhpp1449b";
-BDDs = "0s5a67w9v1lklph8dm4d9bkd6f9qzfb377gvisr3hslacn9ya8zy";
-Bertrand = "05i6xw9gi5ad78rsw5pfhiqllw9x4q4phfi4ddzlxpsgshiw7d0k";
-Buchberger = "1v7zi62ar4inncbcphalsyaggx8im02j81b0fnpvx2x3kyv2pr94";
-CCS = "1na7902k05z19a727wa7rz0dbf1fhcl53r4zxvcgvg5dasvwfc97";
-CFGV = "13gk597r9n2wcgcbhribsqrp9wb8mmr3qd4zbv2ig8469kng0j4m";
-CTLTCTL = "0il1hhizvd2zvh2bhjaa2f43q1qz5sjfdin00yx5l1a8867wjs05";
-CanonBDDs = "1l9yqj0dfqkq49acsy17cvz4rjj86wjbhsdbr4qw2qvn4shllc23";
-Cantor = "1ys81ivigsbsg5cfx9jvm0qprdwc3jm69xm3whq5v9b6skn958yp";
-CatsInZFC = "06rkhns5gz397mafxina52h9z35r0n5bpryk5yfja0kfiyjvp4cr";
-Checker = "0hvfmpy3w4jj4zi3bm9q2yy4361q0lg0znqa22n5l7hzvi28q796";
-Chinese = "191c1bcslxrjxcxvpcz0mzklrl1cwh0lzkd2nq5m0ch3vxar6rq4";
-Circuits = "1a091g5vvmg579mmbfbvhj0scv7zw4n5brmj8dmiwfayfscdh5vg";
-ClassicalRealizability = "1zgivy679rl3ay9mf5ahs0lzrwfg19pcmz5nqm9hq0dpfn9avd6a";
-CoLoR = "05x1drvvhrspj2wzh8v1abblmb9fxy0yx6gg9y4nldkc24widjr7";
-CoRN = "1wv8y67bm2072bd6i3gbvy4sc665sci5kzd1zwv9n2ffxzhy0l5j";
-Coalgebras = "1wzwadfii9mm11bifjbg6f23qbab1ix3valysgq2b4myxlnpwdfz";
-CoinductiveExamples = "1iw6jsxvshsmn52xac3dspkw8f95214f0dcx0y6gi13ln02h8njy";
-CoinductiveReals = "149nsygwlb80s2805qgn85a6mcp7rxifbicbr84l3nyzilfyr6lk";
-ConCaT = "0537r0lamfz657llarxjl030qw29dnya7rb73kx0bdbyphxszr71";
-ConstructiveGeometry = "0cfz64yciyma6jrskc37md4mnv2vbx9hw7y69vyxzy7xdax55j64";
-Containers = "07pjbnzhh418ypppvfkls2x0ycslgl274a913xwi3rb1wrg6q84g";
-Continuations = "0l35xl9kvmq8l9gx3rmcx11p22inw76m1s18y0dnhc6qnhhkq1qg";
-CoqInCoq = "0d5m71xq66rfaa6xr51bsv9hykzfv4dwpclxpnqc7a7ss1q9ccqz";
-Coqoban = "1xp6wblg31asbqbkvbha94lbzn6xnhl0v5y0f3qh4nbmv6hslc54";
-Counting = "150la62c1j4yg8myr7nrp1qwp4z15rfg788j9vraz5q6f2n8c8ph";
-CoursDeCoq = "1qgc03ngzyd138s2cmcwrwrmyq0lf3z3vwhiaq5p371al34fk0d9";
-#Dblib = "00704xi5348fbw9bc0cy5bqx5w4a7aqwpcwdd3740i15ihk60mrl";
-Demos = "0j5ndysvhsj57971yz7xz5mmnzwymgigr3b9mr6nh9iids98g9vy";
-DescenteInfinie = "0is6kclxhfd9n4sdpfkzm4kcc740ifkylg11b8z90frwq79a8yzb";
-Dictionaries = "13zhjvgl20f0hj2pp0zkczm9pwdgh174248jgbqj87rn5alyr2iy";
-DistributedReferenceCounting = "1kw6fb7rvkkrh5rz1839jwf9hrpnrsdnhjlpx3634d5a5kbbdj6a";
-DomainTheory = "1g39bgyxfj9r51vrmrxhrq1xqr36j5q8x0zgz2a12b0k3fj8bswn";
-Ergo = "0xkza35n3f05gkfywaisnis70zsrkh1kwq5idsb2k0rw8m4hq9ki";
-EuclideanGeometry = "11n8877zksgksdfcj7arjx0zcfhsrvg83lcp6yb2bynvfp80gyzb";
-EulerFormula = "1nhh49rf6wza2m5qmz5l5m24m299qn3v80wqzvf51lybadzll2h6";
-ExactRealArithmetic = "1p32g13sx2z5rj3q6390ym8902gvl5x16wdhgz5i75y44s6kmkb1";
-Exceptions = "0w2b16nr80f70dxllmhbqwfr1aw26rcfbak5bdyc0fna8hqp4q3p";
-FOUnify = "1vwp5rwvs5ng4d13l9jjh4iljasfqmc5jpla8rga4v968bp84nw6";
-FSSecModel = "0fi78vqfrw4vrmdw215ic08rw8y6aia901wqs4f1s9z2idd6m8qy";
-FSets = "1n54s2vr6snh31jnvr79q951vyk0w0w6jrnwnlz9d3vyw47la9js";
-Fairisle = "0gg9x69qr0zflaryniqnl8d34kjdij0i55fcb1f1i5hmrwn2sqn6";
-Fermat4 = "0d5lkkrw3vqw6dip1mrgn8imq861xaipirzwpd35jgdkamds802v";
-FingerTree = "1kzfv97mc9sbprgg76lb5lk71gr4a5q10q8yaj57qw3m5hvmdhmw";
-FiringSquad = "0y2dy75j97x0592dxcbcd00ffwnf61f92yiap68xszv3dixl9i9x";
-Float = "1xmskkfd9w3j0bynlmadsrv997988k17bcs0r3zxaazm7vvw2sci";
-FreeGroups = "00pskmp0kfnnafldzcw8vak5v2n0nsjl9pfbw8qkj1xzzbvym2wk";
-FunctionsInZFC = "1vfs27m5f2cx0q2qjlxj3nim1bv53mk241pqz9mpj4plcj0g838l";
-FundamentalArithmetics = "1vvgl5c7rcg3bxizcjdix0fn20vdqy73ixcvm714llb8p986lan5";
-GC = "11kwn43nm58bv7v3p8xg2ih4x0gvgigz26gzh8l8w3lgmriqmzx0";
-GenericEnvironments = "1w05ysx0rl17fgxq3fc0p7p3h70c94qxa6yq88ppyhwm1cqqgihw";
-Goedel = "0b1dfmxp9q5z2l59yz5bn37m0zz4307kq94a7fs8s0lbbwrgyhrf";
-GraphBasics = "1f2bsfkhlyzjvy6ln62sf6hpy9dh8azrnlfpjq6jn667nfb7cbf6";
-Graphs = "0smhsas27llkmfkn4vs8ygb9w19ci2q4ps0f2q969xv8n8n0bj4z";
-GroupTheory = "141w3zbf7jczbk1lrpz6dnpk8yh1vr4f7kw55siawwaai11bh7c1";
-Groups = "00zmn1q9lz7dz8p5wk34svwki9xwn62xkgnhw4bcx8awlbx1pw3a";
-Hardware = "1bp9bnvlv54ksngmgzyxaqw1idxw5snmwrcifqcd6088w6hd9w1n";
-Hedges = "1abbf8v0i8akmhbi2hmb1l9wxvql275c9mxf0r5lzxigwmf0qrbv";
-HighSchoolGeometry = "09n70n0sb1dxnss9xz7xj2z1070gzxs4ap1h0kjcrfkiqss11fpy";
-HigmanCF = "05qg4ci8bvd6s9nmj80imj3b9kfwy4xzfy8ckr5870505mkzxyxv";
-HigmanNW = "0i3mmyh20iib7pglalf4l2p62qyqa6w0mz557n53aa2zx6l0dw18";
-HigmanS = "1c9db1jrpwzqw0arsiljskx3pcxpc1flkdql87fn55lgypbfz5gk";
-HistoricalExamples = "16alm4cv9hj59jyn1rnmb1dnbwp488wpzbnkq6hrnl5drr78gx08";
-HoareTut = "1mazqhb0hclknnzbr4ka1aafkk36hl6n4vixkf5kfvyymr094d0a";
-Huffman = "1h14qdbmawjn9hw813hsywxz0az80nx620rr35mb9wg8hy4xw7jj";
-IEEE754 = "06xrpzg2q9x2bzm7h16k0czm56sgsdn1rxpdgcl44743q3mvpi5p";
-IPC = "1xcgrln8nn2h98qyqz36d0zszjs33kcclv9vamz8mc163agk6jxy";
-IZF = "12inbpihh35hbrh4prs93r4avxlgsj5019n7bndi4fgn09m839bm";
-Icharate = "0giak87mv7g0312i05r7v06wb8wmfkrd2ai54r4c80497f72d17l";
-IdxAssoc = "0gdaxnwyw8phi97izx0wfbpccql73yjdzqqygc4i6nfw4lwanx38";
-IntMap = "1zmlcqv2mz488vpxa6iwbi6sqcljkmb55mywb5pabjjwjj745jhx";
-JProver = "0vz07sclzx0izwm5klwmd0amxhzqly6aknh876vvh3033jp62ik0";
-JordanCurveTheorem = "0varv6ib4f0l3jjq71rafb071ivzcnyxjb5ri8bf6vbjl4fqr335";
-Karatsuba = "02190l3dl0k6qxi3djr2imy4h31kcr5kj94l2ys3xqg1kjjajcmj";
-Kildall = "0lbby3gd3pwivkhr6v8c73915cswmvh50nj3ch10f0zix8lsxrpa";
-LTL = "0bk4232pa6mkbmxjazknfbnmzh2pcjccr68dkf8a2ndd06yfaii1";
-Lambda = "1wy9r95acwf7srs54y5kgmgl9d48j8b871n4z26xpbhdi2pvv9a4";
-Lambek = "0f6nd3fsxsaij9wypwd3cxmgn3larkxg4xww9c0yvjqxpgc5s552";
-LesniewskiMereology = "11wgw93fxwnbvwmpnscvgg9caakhr3wbvqwzqkk1p8wfslpvf7pj";
-LinAlg = "0gl081rx0iikhaghjny3g04aaqgiv0wq6r6c34qpcr5jc6i40mdr";
-MapleMode = "0a50dx473mmg7ksmghbjqs2rg4334dqdd2rkydicw8fl406z19ab";
-Markov = "06aacr8ghycjm68r36hip4rjhwfnbz7az2k8pa92pakjm0am78lq";
-MathClasses = "1gj6dznlc2ma5b5qn9mlinavlrl4xq18dilzd0l9j8jrxfdk1q7n";
-Maths = "15qbv7dxj4ygmw38gnmyf2kwdmy75a21yf991c8lw6fzx334b4dv";
-Matrices = "1q3683xvsgjqlav6kfxx7y05lvr5gp60hpbx4ypwa0hsl6w14mn0";
-#Micromega = "0h2ybdlbdvy30l5kzkfvp5kwsf236fxd3xi87pl4pl3dzylzsbh4";
-MiniC = "1gg9jinay9i3jbsi8bbwxzr9584wycdadf02c5al5yv281ywjar0";
-MiniCompiler = "0yq0k8c0rp120pfssdwfpmz017vq2w8s0rzk9gls476gywjmdvgf";
-MiniML = "1fd4k6rzn5cr24d11dnyy9jp2wf3n8d8l7q7bxk94lbrj6lhrzw2";
-ModRed = "1khg29cm83npasxqlm13bv2w2kfkn9hrvf5q2wch9l1l4ghys4rk";
-Multiplier = "07bj7j4agq2cvhfbkwgrvg39jlzlj1mzlm0ykqjwljd7hi4f6yv9";
-MutualExclusion = "1j3fmf0zvnxg0yzj956jfpjqccnk9l2393q6as80a5gfqhlb3rcr";
-Nfix = "1mpn1fbx15naa2d5lbcxl88xsgp1p88xx4g94f8cjzhg6kdnz7cc";
-OrbStab = "06gg3d2f9qybs2c49mm7srzqx5r9dxail92bcxdi6lr0k74y75ml";
-OtwayRees = "1d39yxppnpzpn5yxdk6rinrgxwgsnr348cggyhwjmgyjm8mr9gcp";
-PAutomata = "0hlzvdi9kb291g36lgyy3vlpn7i8rphpwjisy3wh19j4yqqc7ddf";
-PTS = "12y9niiks4rzpvzzvgfwc1z37480c4l9nvsmh4wx6gsvpnjqvyl3";
-PTSATR = "10jsfbsdaiqrdgp9vnc84wwkxjyfin35kr1qckbax6599xgyk7vj";
-PTSF = "0yz7sh2d4ldcqblnvb96yyimsb4351qqjl8di1cy785mnxa1zfla";
-Paradoxes = "03b22vhkra038z3nfbv9wpbr63x984qyrfvrg58lwqq87s5kgv1d";
-ParamPi = "1p64yj2pqqvyx5b5xm0pv0pm9lqp7hc5hb3wjnwvzi3qchqf7hwi";
-PersistentUnionFind = "1ljdnsm6h3zfn43vla13ibx42kfvgmy6n9qyfn7cgkcw5yv4fh6m";
-PiCalc = "1af8ws86mqs55dldcpm7x4qhk11k0f8l88z2bv6hylfvy6fpbpiy";
-Pocklington = "18zx1ca3pn3vn763smmrnfi395007ddzicrr0cydrph6g4agdw3g";
-Presburger = "1n3nqrplgx1r2vvpcbp91l02c7zc297fkpsqgx1x1msqrldnac9y";
-Prfx = "1nyh134hlh6cdxpys9kv0ngiiibgigh2mifwf8rdz6aj6xj7dgyv";
-ProjectiveGeometry = "01x409rbh3rqxyz53v0kdixnqqv7b890va04a21862g8bml7ls6k";
-QArith = "0xvkw3d3kgiyw6b255f6zbkali1023a9wmn12ga3bgak24jsa8lg";
-QArithSternBrocot = "1kvzww76nxgq7b3b3v2wrjxaxskfrzk55zpg6mj1jjcpgydfqwjr";
-QuicksortComplexity = "0c5gj65rxnxydspc4jqq20c8v9mjbnjrkjkk220yxymbv5n3nqd1";
-RSA = "0b56ipivbbdwc0w7bp4v4lwl0fhhb73k2b62ybmb3x7alc599mc0";
-RailroadCrossing = "0z5cnw1d8jbg30lc9p1hsgrnjwjc4yhpxl74m2pcjscrrnr01zsf";
-Ramsey = "0sd3cihzfx7mn7wcsng15y4jqvp1ql49fy1ch997wfbchp6515ld";
-Random = "0b7gwz38fbk9j5sfa76c2n4781kcb18r65v9vzz8qigx37gm89w4";
-Rational = "0v1zjcf22ij9daxharmaavwp2msgl77y5ad46lskshpypd1ysrsc";
-RecursiveDefinition = "1y4gy2ksxkvmz16zrnblwd1axi7gdjw171n8xfw4f8400my1qhm0";
-ReflexiveFirstOrder = "156a6kmds25kc645w6kkhn3a4bvryp307b76ghz5m5wv2wsajgrn";
-RegExp = "0gya2kckr6325hykd12vwpbwwf7cf04yyjrr2dvmcc81dkygrwxb";
-RelationAlgebra = "1nrhkvypkk7k48gb18c2q9cwbgy02ldfg6s3j74f5rgff1i6c9in";
-RelationExtraction = "1g6hvmsfal17pppqf9v8zh2i1dph0lj5a1r3xiszqr4biiig09ch";
-ReleasedSsreflect = "17wirznfsizmw6gjb54vk9bp97a3bc1l2sb4gdxfbzvxmabx1a9l";
-Rem = "03559q60ibf4dr1np82341xfrw134d27dx8dim84q9fszr4gy8sx";
-RulerCompassGeometry = "02vm80xvvw22pdxrag3pv5zrhqf8726i9jqsiv4bnjqavj5z2hdr";
-SMC = "0ca3ar1y9nyj5147r18babqsbg2q2ywws8fdi91xb5z9m3i97nv1";
-Schroeder = "0mfbjmw4a48758k88yv01494wnywcp5yamkl394axvvbbna9h8b6";
-SearchTrees = "1jyps6ddm8klmxjm50p2j9i014ij7imy3229pwz3dkzg54gxzzxb";
-Semantics = "157db1y5zgxs9shl7rmqg89gxfa4cqxwlf6qys0jh3j0wsxs8580";
-Shuffle = "14v1m4s9k49w30xrnyncjzgqjcckiga8wd2vnnzy8axrwr9zq7iq";
-SquareMatrices = "07dlykg3w59crc54qqdqxq6hf8rmzvwwfr1g8z8v2l8h4yvfnhfl";
-Ssreflect = "07hv0ixv68d8vrpf9s6gxazxaz5fwpmhqrd6cqw7xp8m8gspxifz";
-Stalmarck = "0vcbkzappq1si4hxbnb9bjkfk82j3jklb8g8ia83h1mdhzr7xdpz";
-Streams = "1spcqnvwayahk12fd13vzh922ypzrjkcmws9gcy12qdqp04h8bnc";
-String = "1wy7g66yq9y8m8y3gq29q7whfdm98g3cj9jxm5yibdzfahfdzzni";
-Subst = "1wxscjhz2y2jv5rdga80ldx2kc954sklip4jsbsd2fim5gwxzl23";
-Sudoku = "0f9h8gwzrdzk5j76nhvlnvpll81zar3pk84r2bf1xfav4yvj8sj7";
-SumOfTwoSquare = "1lxf9wdmvpi0vz4d21p6v9h2vvkk9v8113mvr2cdxd0j43l4ra18";
-Tait = "0bwxl894isndwadbbc3664j51haj3c0i57zmmycnxmhnmsx5pnjj";
-TarskiGeometry = "1vkznrjla943wcyddzyq0pqraiklgn62n1720msxp7cs13ckzpy0";
-ThreeGap = "01nj27xs348126ynsnva1jnvk0nin61xzyi6hwcybj5n46r7nlcv";
-Topology = "1kchddfiksjnkvwdr2ffpqcvmqkd6gf359r09yngf340sa15p5wk";
-TortoiseHareAlgorithm = "1ldm1z48j59lxz60szpy64d0928j4fmygp5npfksvwkvghijchq8";
-TreeAutomata = "0jzfa6rxv7lw1nzrqaxv08h9mpyvc2g4cbdc09ncyhazincrix0z";
-TreeDiameter = "0xdansrbmxrwicvqjjr9ivgs0255nd4ic6jkfv37m1c10vxcjq2n";
-WeakUpTo = "1baaapciaqhyjx8bqa4l04l1vwycyy1bvjr2arrc9myqacifmnpp";
-ZChinese = "0v7gffmcj9yazbbssb2i2iha1dr82b4bl8df9g021s40da49k09k";
-ZF = "0am15lgpn127pzx6ghm76axy75w7m9a8wqa26msgkczjk4x497ni";
-ZFC = "0s11g9rzacng2xg9ygx9lxyqv2apxyirnf7cg3iz95531n46ppn2";
-ZSearchTrees = "1lh6jlzm53jnsg91aa60f6gir6bsx77hg8xwl24771jg8a9b9mcl";
-ZornsLemma = "0dxizjfjx4qsdwc60k6k9fnq8hj4m13vi0llsv9xk3lj3izhpil1";
-lazyPCF = "0wzpv41nv3gdd07g9pr7wydfjv1wxz8kylzmyn07ab38kahhhzh9";
-lc = "05zr0y2ivznmf1ijszq249v4rw6kvdx6jz4s2hhnaiqvx35g4cqg";
-}
diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix
deleted file mode 100644
index 289a4d759214..000000000000
--- a/pkgs/development/coq-modules/contribs/default.nix
+++ /dev/null
@@ -1,261 +0,0 @@
-contribs:
-
-let
-  mkContrib = import ./mk-contrib.nix;
-  all = import ./all.nix;
-  overrides = {
-    Additions = self: {
-      patchPhase = ''
-        for p in binary_strat dicho_strat generation log2_implementation shift
-        do
-          substituteInPlace $p.v \
-          --replace 'Require Import Euclid.' 'Require Import Coq.Arith.Euclid.'
-        done
-      '';
-    };
-    BDDs = self: {
-      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../../Cachan/IntMap IntMap
-        32d30
-        < extraction
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-      postInstall = ''
-        mkdir -p $out/bin
-        cp extraction/dyade $out/bin
-      '';
-    };
-    CanonBDDs = self: {
-      patchPhase = ''
-        patch Make <<EOF
-        17d16
-        < rauzy/algorithme1/extraction
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-      postInstall = ''
-        mkdir -p $out/bin
-        cp rauzy/algorithme1/extraction/suresnes $out/bin
-      '';
-    };
-    CoinductiveReals = self: {
-      buildInputs = self.buildInputs ++ [ contribs.QArithSternBrocot ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../QArithSternBrocot QArithSternBrocot
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    CoRN = self: {
-      buildInputs = self.buildInputs ++ [ contribs.MathClasses ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../MathClasses/ MathClasses
-        EOF
-        coq_makefile -f Make -o Makefile.coq
-      '';
-      enableParallelBuilding = true;
-      installFlags = self.installFlags + " -f Makefile.coq";
-    };
-    Counting = self: {
-      postInstall = ''
-        for ext in cma cmxs
-        do
-          cp src/counting_plugin.$ext $out/lib/coq/8.4/user-contrib/Counting/
-        done
-      '';
-    };
-    Ergo = self: {
-      buildInputs = self.buildInputs ++ (with contribs; [ Containers Counting Nfix ]);
-      patchPhase = ''
-        patch Make <<EOF
-        4,9d3
-        < -I ../Containers/src
-        < -R ../Containers/theories Containers
-        < -I ../Nfix/src
-        < -R ../Nfix/theories Nfix
-        < -I ../Counting/src
-        < -R ../Counting/theories Counting
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    FingerTree = self: {
-      patchPhase = ''
-        patch Make <<EOF
-        21d20
-        < extraction
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    FOUnify = self: {
-      patchPhase = ''
-        patch Make <<EOF
-        8c8
-        < -custom "\$(CAMLOPTLINK) -pp '\$(CAMLBIN)\$(CAMLP4)o' -o unif unif.mli unif.ml main.ml" unif.ml unif
-        ---
-        > -custom "\$(CAMLOPTLINK) -pp 'camlp5o' -o unif unif.mli unif.ml main.ml" unif.ml unif
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-      postInstall = ''
-        mkdir -p $out/bin
-        cp unif $out/bin/
-      '';
-    };
-    Goedel = self: {
-      buildInputs = self.buildInputs ++ [ contribs.Pocklington ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../../Eindhoven/Pocklington Pocklington
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    Graphs = self: {
-      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../../Cachan/IntMap IntMap
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-      postInstall = ''
-        mkdir -p $out/bin
-        cp checker $out/bin/
-      '';
-    };
-    IntMap = self: { configurePhase = "coq_makefile -f Make -o Makefile"; };
-    LinAlg = self: {
-      buildInputs = self.buildInputs ++ [ contribs.Algebra ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../../Sophia-Antipolis/Algebra/ Algebra
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    Markov = self: { configurePhase = "coq_makefile -o Makefile -R . Markov markov.v"; };
-    Nfix = self: {
-      postInstall = ''
-        for ext in cma cmxs
-        do
-          cp src/nfix_plugin.$ext $out/lib/coq/8.4/user-contrib/Nfix/
-        done
-      '';
-    };
-    OrbStab = self: {
-      buildInputs = self.buildInputs ++ (with contribs; [ LinAlg Algebra ]);
-      patchPhase = ''
-        patch Make <<EOF
-        2,3d1
-        < -R ../../Sophia-Antipolis/Algebra Algebra
-        < -R ../../Nijmegen/LinAlg LinAlg
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    PTSF = self: {
-      buildInputs = self.buildInputs ++ [ contribs.PTSATR ];
-      patchPhase = ''
-        patch Make <<EOF
-        1d0
-        < -R ../../Paris/PTSATR/ PTSATR
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    RelationExtraction = self: {
-      patchPhase = ''
-        patch Make <<EOF
-        31d30
-        < test
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    Semantics = self: {
-      patchPhase = ''
-        patch Make <<EOF
-        18a19
-        > interp.mli
-        EOF
-      '';
-      configurePhase = ''
-        coq_makefile -f Make -o Makefile
-        make extract_interpret.vo
-        rm -f str_little.ml.d
-      '';
-    };
-    SMC = self: {
-      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../../Cachan/IntMap IntMap
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    Ssreflect = self: {
-      patchPhase = ''
-        substituteInPlace Makefile \
-        --replace "/bin/mkdir" "mkdir"
-      '';
-    };
-    Stalmarck = self: {
-      configurePhase = "coq_makefile -R . Stalmarck *.v staltac.ml4 > Makefile";
-    };
-    Topology = self: {
-      buildInputs = self.buildInputs ++ [ contribs.ZornsLemma ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../ZornsLemma ZornsLemma
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-    TreeAutomata = self: {
-      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
-      patchPhase = ''
-        patch Make <<EOF
-        2d1
-        < -R ../../Cachan/IntMap IntMap
-        EOF
-        coq_makefile -f Make -o Makefile
-      '';
-    };
-  };
-in
-
-callPackage: extra:
-
-builtins.listToAttrs (
-map
-(name:
-  let
-    sha256 = builtins.getAttr name all;
-    override =
-      if builtins.hasAttr name overrides
-      then builtins.getAttr name overrides
-      else x: { };
-  in
-  {
-    inherit name;
-    value = callPackage (mkContrib { inherit name sha256 override; }) extra;
-  }
-)
-(builtins.attrNames all)
-)
diff --git a/pkgs/development/coq-modules/contribs/mk-contrib.nix b/pkgs/development/coq-modules/contribs/mk-contrib.nix
deleted file mode 100644
index 12dd700a6310..000000000000
--- a/pkgs/development/coq-modules/contribs/mk-contrib.nix
+++ /dev/null
@@ -1,30 +0,0 @@
-{ name, sha256, override }:
-
-{ stdenv, fetchzip, coq }:
-
-let
-  self = {
-
-  name = "coq-contribs-${name}-${coq.coq-version}";
-
-  src = fetchzip {
-    url = "http://www.lix.polytechnique.fr/coq/pylons/contribs/files/${name}/v${coq.coq-version}/${name}.tar.gz";
-    inherit sha256;
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = with stdenv.lib; {
-    homepage = "http://www.lix.polytechnique.fr/coq/pylons/contribs/view/${name}/v${coq.coq-version}";
-    maintainers = with maintainers; [ vbgl ];
-    platforms = coq.meta.platforms;
-  };
-
-};
-
-in
-
-stdenv.mkDerivation (self // override self)
diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix
index 5ebf07922776..374979f1d15b 100644
--- a/pkgs/development/coq-modules/coq-ext-lib/default.nix
+++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix
@@ -2,7 +2,6 @@
 
 let param =
   {
-    "8.4" = { version = "0.9.0"; sha256 = "1n3bk003vvbghbrxkhal6drnc0l65jv9y77wd56is3jw9xgiif0w"; };
     "8.5" = { version = "0.9.4"; sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; };
     "8.6" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; };
     "8.7" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; };
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
deleted file mode 100644
index b6d3fe2e34f3..000000000000
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ /dev/null
@@ -1,33 +0,0 @@
-{ stdenv, fetchgit, coq, mathcomp }:
-
-stdenv.mkDerivation rec {
-
-  name = "coq-coqeal-${coq.coq-version}-${version}";
-  version = "7522037d";
-
-  src = fetchgit {
-    url = git://github.com/CoqEAL/CoqEAL.git;
-    rev = "7522037d5e01e651e705d782f4f91fc68c46866e";
-    sha256 = "0kbnsrycd0hjni311i8xc5xinn4ia8rnqi328sdfqzvvyky37fgj";
-  };
-
-  propagatedBuildInputs = [ mathcomp ];
-
-  preConfigure = ''
-    cd theory
-    patch ./Make <<EOF
-    0a1
-    > -R . CoqEAL
-    EOF
-  '';
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = with stdenv.lib; {
-    homepage = http://www.maximedenes.fr/content/coqeal-coq-effective-algebra-library;
-    description = "A Coq library for effective algebra, by which is meant formally verified computer algebra algorithms that can be run inside Coq on concrete inputs";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index 84f95d4ddea3..7f5111462bd5 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -1,27 +1,11 @@
 { stdenv, fetchurl, which, coq, ssreflect }:
 
-let param =
-  let
-  v2_1_1 = {
-    version = "2.1.1";
-    url = https://gforge.inria.fr/frs/download.php/file/35429/coquelicot-2.1.1.tar.gz;
-    sha256 = "1wxds73h26q03r2xiw8shplh97rsbim2i2s0r7af0fa490bp44km";
-  };
-  v3_0_1 = {
-    version = "3.0.1";
+stdenv.mkDerivation {
+  name = "coq${coq.coq-version}-coquelicot-3.0.1";
+  src = fetchurl {
     url = "https://gforge.inria.fr/frs/download.php/file/37045/coquelicot-3.0.1.tar.gz";
     sha256 = "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r";
   };
-  in {
-  "8.4" = v2_1_1;
-  "8.5" = v3_0_1;
-  "8.6" = v3_0_1;
-  "8.7" = v3_0_1;
-}."${coq.coq-version}"; in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-coquelicot-${param.version}";
-  src = fetchurl { inherit (param) url sha256; };
 
   nativeBuildInputs = [ which ];
   buildInputs = [ coq ];
diff --git a/pkgs/development/coq-modules/domains/darcs_context b/pkgs/development/coq-modules/domains/darcs_context
deleted file mode 100644
index 5dac711c0c0a..000000000000
--- a/pkgs/development/coq-modules/domains/darcs_context
+++ /dev/null
@@ -1,809 +0,0 @@
-
-Context:
-
-[additional facts about limits on cuts
-robdockins@fastmail.fm**20140818025955
- Ignore-this: 6f9c952db425df6ae9d2a14139a8a3d1
-] 
-
-[work on limits
-robdockins@fastmail.fm**20140817221707
- Ignore-this: 9811e0cd669b48f3beb7a56d47cbe3c3
-] 
-
-[finish proving that Q field ops commute with injq
-robdockins@fastmail.fm**20140817060600
- Ignore-this: a1f6c62b39983e6f6f01d28aca5f8534
-] 
-
-[split up realdom.v and perform associated code motion
-robdockins@fastmail.fm**20140817030034
- Ignore-this: 24c74cd459d2ab15dcd3d83ba06f7081
-] 
-
-[recip is canonical and converges
-robdockins@fastmail.fm**20140725211947
- Ignore-this: c100dbd94114cca9576b2a3f46c9ddc7
-] 
-
-[improve the proof that 1 is a unit for multiplication
-robdockins@fastmail.fm**20140724150124
- Ignore-this: c5ec976f8a9858a7ba1f704b4e84d02e
-] 
-
-[complete proof the interval multiplication converges; other minor stuff
-robdockins@fastmail.fm**20140724015132
- Ignore-this: bc717baa4c8f9ec31b821c5cfae5b499
-] 
-
-[further progress in realdom.v
-robdockins@fastmail.fm**20140723004023
- Ignore-this: f33e18d22ae69c9b6209e28151d18017
-] 
-
-[unmessify rational_intervals patch
-robdockins@fastmail.fm**20140721123718
- Ignore-this: 4a125b192a9964a508a1063845e9f160
-] 
-
-[messy updates to rational_intervals.v
-robdockins@fastmail.fm**20140721015810
- Ignore-this: 858dac9c55426167c6f397a71ef3fda5
-] 
-
-[implicit arguments for "fixes"
-robdockins@fastmail.fm**20140721015739
- Ignore-this: 229ecdd48265fc855319141e399bc522
-] 
-
-[metadata
-robdockins@fastmail.fm**20140714201441
- Ignore-this: aa16faaf09c1c404bdc6eaf0d0c39912
-] 
-
-[further beautification
-robdockins@fastmail.fm**20140714200516
- Ignore-this: 47d74c51d9fe130a5ac12706b1ddb1d4
-] 
-
-[start working on the recripricol function
-robdockins@fastmail.fm**20140714180055
- Ignore-this: c7f93cea17f46daa78a1ea14e86dfcaf
-] 
-
-[tweaks to the lambda models
-robdockins@fastmail.fm**20140714180031
- Ignore-this: 219788fe70f42f0f6e60176cab464f19
-] 
-
-[beauty edits in st_lam*
-robdockins@fastmail.fm**20140714180006
- Ignore-this: a40aa7ae00ed27595ee04073918bd028
-] 
-
-[move stuff to rational_intervals.v / define real_mult and prove some properties
-robdockins@fastmail.fm**20140712053232
- Ignore-this: 398c5c03aac9ff37526d4d7c9e1a82c0
-] 
-
-[finish correctness proof for interval multiplication
-robdockins@fastmail.fm**20140711191547
- Ignore-this: c9ab138a0ca43fe0b133b208419bbcc4
-] 
-
-[break out facts about rational intervals
-robdockins@fastmail.fm**20140711012320
- Ignore-this: b7fe6e9377629a89b5debe3019ae1aa
-] 
-
-[updates to ideal completion
-robdockins@fastmail.fm**20140707053800
- Ignore-this: 90d1efbd0e5833d8c83f0df056d7a74c
-] 
-
-[a pile of additional properties in realdom.v
-robdockins@fastmail.fm**20140707053519
- Ignore-this: 7edba1e72a1856f297ef11e698ed989f
-] 
-
-[some properties of converging prereals
-robdockins@fastmail.fm**20140706041401
- Ignore-this: 273bfbb245302becd7ff402831827ffb
-] 
-
-[make realdom compile
-robdockins@fastmail.fm**20140630015439
- Ignore-this: 8bfc8eaeed4a1596450b0bb9ddef9aaa
-] 
-
-[renaming
-robdockins@fastmail.fm**20140630011639
- Ignore-this: a287e083af095790cbf2b48df7a58739
-] 
-
-[reorganize some code
-robdockins@fastmail.fm**20140630011446
- Ignore-this: f1375b9e7ad822cb92f0c83d4001eddd
-] 
-
-[build the retract for realdom
-robdockins@fastmail.fm**20140630001245
- Ignore-this: 4eb9da621588417d1b7b2fc980c7bf70
-] 
-
-[fill out lemmas about cPLT
-robdockins@fastmail.fm**20140630001140
- Ignore-this: add9e45c14621e3d6328684098bf8461
-] 
-
-[more facts about cPLT
-robdockins@fastmail.fm**20140628073731
- Ignore-this: 101a131ed114902924a1707eff7ebc70
-] 
-
-[continuous domains as retracts of bifinite domains
-robdockins@fastmail.fm**20140628035522
- Ignore-this: 5e7c61d49cf8424412b0d94f5fcb5ee6
-] 
-
-[start implementing arithmetic operations in RealDom
-robdockins@fastmail.fm**20140620003249
- Ignore-this: c28479b8a933cba263765bdddb112264
-] 
-
-[define the domain of rational intervals
-robdockins@fastmail.fm**20140619040809
- Ignore-this: 6cbe1a9cc690e5a9d77f37ee299154b
- this domain is useful for describing the semantics of exact real arithmetic.
-] 
-
-[show that every effective CUSL is Plotkin
-robdockins@fastmail.fm**20140619034433
- Ignore-this: d529a4b1d6d698f79572caa805072394
-] 
-
-[fix notation for octothorpe
-robdockins@fastmail.fm**20140614222130
- Ignore-this: 3dc815825f11ceaf4f4f53e4668e6382
-] 
-
-[fix for coq 8.4pl4
-robdockins@fastmail.fm**20140614222049
- Ignore-this: 9745904845aaf54e5569df982fc93d65
-] 
-
-[move swelling lemma into finsets
-robdockins@fastmail.fm**20140504080535
- Ignore-this: ffa560e9aa4e4f8b15a55c1f9b1da72e
-] 
-
-[documentation improvements and code motion
-robdockins@fastmail.fm**20140504070008
- Ignore-this: da7847f82403990342732a8ce226315c
-] 
-
-[replace the old finprod
-robdockins@fastmail.fm**20140504005534
- Ignore-this: 606cf44422f68d66c8d2d90049e67b93
-] 
-
-[remove the old finprod
-robdockins@fastmail.fm**20140504005137
- Ignore-this: 38bd54e16c87d27bbede08496c37bfba
-] 
-
-[update st_lam_fix to use the new finprod
-robdockins@fastmail.fm**20140504003627
- Ignore-this: 95d0a66e99ccead89bdfef09a1c8c109
-] 
-
-[update st_lam to use the new termmodel
-robdockins@fastmail.fm**20140503230854
- Ignore-this: c3d6b2155674b414c5c2e14b85b13760
-] 
-
-[new version of finprod with a better term model
-robdockins@fastmail.fm**20140503222035
- Ignore-this: db63e3a063bdb6f2f579644c7b63bd1b
-] 
-
-[a few more (hopefully final) lemmas about union
-robdockins@fastmail.fm**20140422223924
- Ignore-this: 7b95c75abef9b0d45863b5e33d1c5a37
-] 
-
-[finish proofs about union
-robdockins@fastmail.fm**20140422065034
- Ignore-this: 2929c3cdb013c028a48022b0293b2f18
-] 
-
-[powerdomain progress
-robdockins@fastmail.fm**20140421064325
- Ignore-this: 592f9c6046f05a27897b460edb2efe10
- Show that powerdomains are endofunctors on PLT.  Further, they are monads with
- the 'singleton' and 'join' operations.  Also make some progress on the additive
- portion of the theory, dealing with emptyset and union.
-] 
-
-[tweak makefile
-robdockins@fastmail.fm**20140420031337
- Ignore-this: d5954b26f731bfed3d79cefacab322fb
-] 
-
-[show that semvalue is the weakest condition allowing beta-reduction of strict functions
-robdockins@fastmail.fm**20140420020447
- Ignore-this: 16a7ed23f04879f1fb324bdac8a2ffaf
-] 
-
-[some additional operations relating to the PLT adjunction
-robdockins@fastmail.fm**20140420020351
- Ignore-this: db8eec6e3f74cce3acb67d2b660b104e
-] 
-
-[finish building power domain fmap
-robdockins@fastmail.fm**20140420020217
- Ignore-this: 556e1cb87576de36cb26f8add3a1b163
-] 
-
-[fix up st_lam.v
-robdockins@fastmail.fm**20140329015058
- Ignore-this: 1c31d674b759fbd0cc74fb3125579f96
-] 
-
-[push some proofs into finprod
-robdockins@fastmail.fm**20140329000401
- Ignore-this: 49070fdd951e49473e60d3cd0ec431c6
-] 
-
-[documentation and aesthetic changeds
-robdockins@fastmail.fm**20140327043141
- Ignore-this: be27b24b78ea6af722a307117e59f5b3
-] 
-
-[finish the st_lam_fix example
-robdockins@fastmail.fm**20140322011153
- Ignore-this: e702f564b6eab2f8c11ab16bcb62504b
-] 
-
-[clarafications re: countable choice; remove unfinished example from build order
-robdockins@fastmail.fm**20140321212852
- Ignore-this: 2a9d5c79c05ba088e1815feab99a5f6c
-] 
-
-[break the "fixes" operator into a separate file and prove some facts about it
-robdockins@fastmail.fm**20140318013247
- Ignore-this: 80c506cef0719a974a049a1f5870f676
-] 
-
-[minor fix to skiy.v
-robdockins@fastmail.fm**20140317054057
- Ignore-this: ffef6fcaf5fa7f8cea80d2808caf4f4c
-] 
-
-[add the fixpoint operator; admit proofs
-robdockins@fastmail.fm**20140317044648
- Ignore-this: 97ca18e980cdf46a9b40c8252badef14
-] 
-
-[remove the evaluation case for variables
-robdockins@fastmail.fm**20140317032932
- Ignore-this: e46d634e735e5b21a18518a48777168d
-] 
-
-[start on STLC with fixpoints -- but without fixpoints for now 
-robdockins@fastmail.fm**20140317031953
- Ignore-this: 3458bc18c73d967bef58418bc73e06cb
-] 
-
-[add the eliminator for booleans to st_lam; other additional utility lemmas
-robdockins@fastmail.fm**20140317031753
- Ignore-this: 369dd375755cbd9ae5e3c969f3ef6ec
-] 
-
-[some minor code motion
-robdockins@fastmail.fm**20140228064927
- Ignore-this: 804828472ddb0c5fafc72460fce8387b
-] 
-
-[plug final holes in st_lam and add to build order
-robdockins@fastmail.fm**20140228044729
- Ignore-this: 3edc7f36bfa97775ba33ffa27c80df59
-] 
-
-[reduce st_lam.v to facts I believe about fresh variables
-robdockins@fastmail.fm**20140228010832
- Ignore-this: bde3e73291ddd32337d6fb999e4b1c02
-] 
-
-[fix breakages
-robdockins@fastmail.fm**20140226073930
- Ignore-this: 9be54f5255f8ed9d53a79260e9bdf565
-] 
-
-[more work on lambdas
-robdockins@fastmail.fm**20140226043753
- Ignore-this: 7f7452670221e2643067a3c7cc180998
-] 
-
-[use new finprod implementation
-robdockins@fastmail.fm**20140226043700
- Ignore-this: c9e05df5fcfd31254ed7318fe693490c
-] 
-
-[remove old finprod 
-robdockins@fastmail.fm**20140226043642
- Ignore-this: 2705703a2c782da21a152fbb27c8a972
-] 
-
-[rearrange the interfact to finprod
-robdockins@fastmail.fm**20140226043541
- Ignore-this: c44d7c478948f42b188eb8d06469abbf
-] 
-
-[fill remaining holes in finprod2
-robdockins@fastmail.fm**20140225205242
- Ignore-this: 1eeb9b8beef92790c28918292f2a9cf4
-] 
-
-[rework some stuff dealing with semidecidable predicates
-robdockins@fastmail.fm**20140225092149
- Ignore-this: 32b5ccb2927e08979ea92b9ef67c40f4
-] 
-
-[lots of work on alpha-congrunce in lambdas
-robdockins@fastmail.fm**20140225035601
- Ignore-this: fbbec9dac4cb328ff4e0b25df646e0c7
-] 
-
-[terminate is universal in PLT
-robdockins@fastmail.fm**20140225035538
- Ignore-this: abc6cd1a60578c435bf9ca596d8d0922
-] 
-
-[new attack on nominal finite products
-robdockins@fastmail.fm**20140225035516
- Ignore-this: 3875e713acc6aa5193696612f3ede76d
-] 
-
-[push forward a little on lambdas
-robdockins@fastmail.fm**20140221095249
- Ignore-this: c690a1b03075702e3fd84aac7e268211
-] 
-
-[update finprod for various changes
-robdockins@fastmail.fm**20140221095230
- Ignore-this: a6d787930ed356ae2b0a003af1f4d44
-] 
-
-[better discrete cases lemma
-robdockins@fastmail.fm**20140219051301
- Ignore-this: f0ec88e8207257e7657ced933cf687e7
-] 
-
-[start working on simply-typed lambdas
-robdockins@fastmail.fm**20140219051238
- Ignore-this: 69bea345376ea39cd1addc0849a43077
-] 
-
-[more messing about with advanced category theory stuff
-robdockins@fastmail.fm**20140211095003
- Ignore-this: 9cd3c9d961349e8797f109f716c5f678
-] 
-
-[minor rearrangements and code motion
-robdockins@fastmail.fm**20140211041724
- Ignore-this: 642ad6f1395fde7ecd81e5a905fd5428
-] 
-
-[some basic bicategory theory
-robdockins@fastmail.fm**20140210083634
- Ignore-this: f47a898fa045a397d3ee70e1512b8baa
-] 
-
-[even more notation futzing
-robdockins@fastmail.fm**20140209072416
- Ignore-this: d2061652cb3e80f6994f567a9e677b32
-] 
-
-[additional notational futzing
-robdockins@fastmail.fm**20140209043308
- Ignore-this: ac42cbbc94df227e6d5e70b96ae65fd3
-] 
-
-[futz around with notations, various other cleanup activities
-robdockins@fastmail.fm**20140209005551
- Ignore-this: 3f41a52650aadd956ac490b62e59c1c3
-] 
-
-[complete adequacy for SKI+Y
-robdockins@fastmail.fm**20140206050414
- Ignore-this: f730587ac7a42f3e35740976a1439f2e
-] 
-
-[minor changes in cpo
-robdockins@fastmail.fm**20140206014745
- Ignore-this: 95244704faf1e6c336d62dc7912f9022
-] 
-
-[push through most of SKI+Y adequacy
-robdockins@fastmail.fm**20140205214805
- Ignore-this: dc998ef45f2e919e9373bfa21a5ef8c7
-] 
-
-[major simplification of the adequacy proof for SKI
-robdockins@fastmail.fm**20140205185605
- Ignore-this: f1f0dc46274db05f3393038dfe2775e2
-] 
-
-[push forward on SKI+Y
-robdockins@fastmail.fm**20140205044216
- Ignore-this: daf255aa940b42c1c68ba947a356370d
-] 
-
-[continue futzing with the LR statement
-robdockins@fastmail.fm**20140203055601
- Ignore-this: f5ef9f06d3b1a11d76317b52cec691ab
-] 
-
-[start pushing on adequacy for SKI+Y
-robdockins@fastmail.fm**20140202085948
- Ignore-this: 956844809340fad0c13c19e9fa729b5c
-] 
-
-[mostly finish soundness for SKI+Y
-robdockins@fastmail.fm**20140202060633
- Ignore-this: 4c75fd9eeefa1d6dad6866662abea0fd
-] 
-
-[start working on a CCL example
-robdockins@fastmail.fm**20140202020748
- Ignore-this: 44c5d7854cc19b0f90414c2be6b3df68
-] 
-
-[make id(A) a parsing-only notation
-robdockins@fastmail.fm**20140202020724
- Ignore-this: 68f51f754c0b89e2e815da47b901e4b1
-] 
-
-[the PLT adjunction is strong monodial
-robdockins@fastmail.fm**20140202020637
- Ignore-this: 7b29b9a6a5e8efa07440c528ec12d7bd
-] 
-
-[fix my broken version of lfp and fixup proofs
-robdockins@fastmail.fm**20140202020615
- Ignore-this: 3ac283481318622cbf38378e815a4f09
-] 
-
-[more work on SKI + Y
-robdockins@fastmail.fm**20140202020516
- Ignore-this: d1f63e2ef610c6f93d03806c5426cfa5
-] 
-
-[start work on SKI + Y
-robdockins@fastmail.fm**20140201085039
- Ignore-this: fb7a405830cf90526cddd8ce37f4da40
-] 
-
-[doc corrections
-robdockins@fastmail.fm**20140130015908
- Ignore-this: bca4c04267bfdac8cb202651a0960d92
-] 
-
-[lots of additional inline documentation
-robdockins@fastmail.fm**20140129234834
- Ignore-this: ab2c59add5514f44a898de1f0eece98b
-] 
-
-[powerdomains form continuous functors in EMBED
-robdockins@fastmail.fm**20140126234115
- Ignore-this: d2ee08902f0bdb52efd7f7ce2c594469
-] 
-
-[complete the powerdomain constructions; build some operations
-robdockins@fastmail.fm**20140125225202
- Ignore-this: 9c8f2632df05e84fc3794a338ff8720d
-] 
-
-[construct the basic powerdomains--still some holes left 
-robdockins@fastmail.fm**20140125064541
- Ignore-this: c3206d2e1e925096b3e9ff49afacef2f
-] 
-
-[generalize the lfp construction to a generic chain_sup operation
-robdockins@fastmail.fm**20140124183103
- Ignore-this: 4cc2c1011b9f79365dcb7c76784fbfa6
-] 
-
-[update makefile
-robdockins@fastmail.fm**20140124073734
- Ignore-this: a0b7db8383262caa314c21b99e146222
-] 
-
-[new file for recursive lambda domains
-robdockins@fastmail.fm**20140124070023
- Ignore-this: 300c02b4da83b6ebd734aa2ccb21cd2d
-] 
-
-[more lemmas about antistrict homs
-robdockins@fastmail.fm**20140124065953
- Ignore-this: 483c7b350dc3cab59c8ff50e1ac73b8c
-] 
-
-[fix breakage related to implicit arguments
-robdockins@fastmail.fm**20140124065805
- Ignore-this: 561693d3280851299c6a49a2a34546b3
-] 
-
-[notation tweaks in cpo.v
-robdockins@fastmail.fm**20140124053800
- Ignore-this: 83e92d8c14568448074a940ceafbe2c9
-] 
-
-[add if/then/else to the SKI system
-robdockins@fastmail.fm**20140124023630
- Ignore-this: 37a9737932a05393a6338380226ca346
-] 
-
-[case analysis for finite types
-robdockins@fastmail.fm**20140124012505
- Ignore-this: 6ec1076b2a74f5832501a105a28a6dba
-] 
-
-[finish adequacy proof for SKI
-robdockins@fastmail.fm**20140123211322
- Ignore-this: 1fe3e626e33431c27e2aa186b3bf91d2
-] 
-
-[additional lemmas about domains
-robdockins@fastmail.fm**20140123090037
- Ignore-this: fcad2dd816f805b8b5e7d1be3df60db8
-] 
-
-[most of a proof of adequacy for SKI
-robdockins@fastmail.fm**20140123085839
- Ignore-this: d1595c02a6387297018e7f316a3e751
-] 
-
-[more work on finite products
-robdockins@fastmail.fm**20140121061158
- Ignore-this: c2f8212e041478104dd4c81c225b42d5
-] 
-
-[begin work on a more flexible "finprod" domain
-robdockins@fastmail.fm**20140119021653
- Ignore-this: 249718a2c31964733171b21c84d2effb
-] 
-
-[mess with implicit arguments in categories.v
-robdockins@fastmail.fm**20140113041450
- Ignore-this: 314cad9207f706e949bd686aaa5c5e1b
-] 
-
-[products for CPO, uniformity of lfp
-robdockins@fastmail.fm**20140113041421
- Ignore-this: e533abe995e634c732a35e71d66ddb6a
-] 
-
-[define the LFP in pointed CPOs, prove the Scott induction principle
-robdockins@fastmail.fm**20140112231843
- Ignore-this: 2014174b1c6914bef376d614f34d073f
-] 
-
-[build the forgetful functor from EMBED to PLT
-robdockins@fastmail.fm**20140110014909
- Ignore-this: 1dacbfc0383e48f4ab35fe0a5fd11cec
-] 
-
-[notation changes, prove sum_cases and curry preserve order and equality
-robdockins@fastmail.fm**20140110014820
- Ignore-this: d1c6a1d0346a9eba14f3529ac30b5e2f
-] 
-
-[prove addl facts about pairs, tweak implicit arguments
-robdockins@fastmail.fm**20140110010319
- Ignore-this: 9f0af8abc268b2b22d8b5450d6a4136
-] 
-
-[make 'ob' a coercion
-robdockins@fastmail.fm**20140110010204
- Ignore-this: 467c0b0a8b086a7f44bf98875a4380d6
-] 
-
-[copyright notices
-robdockins@fastmail.fm**20140106232333
- Ignore-this: f59bafa0ec99e259bd9b4319f2cdbc67
-] 
-
-[add ord_dec coercion
-robdockins@fastmail.fm**20140104052750
- Ignore-this: 4ed1cacfd27979f0fe518862be5ac27c
-] 
-
-[define the model for CBV lambda calculus
-robdockins@fastmail.fm**20140104050626
- Ignore-this: 88ca796d4697bfebb044d3fae27d6129
-] 
-
-[proof a fixpoint lemma for unpointed domains
-robdockins@fastmail.fm**20140103231818
- Ignore-this: 4939eb02d09b6a4eecf145c887c64393
-] 
-
-[prove that the adjoint functors between PLT and PPLT extend to continuous functors in EMBED
-robdockins@fastmail.fm**20140103000915
- Ignore-this: 54da0101f581731ebe512ed514e0603e
-] 
-
-[notation changes for PLT
-robdockins@fastmail.fm**20140102234446
- Ignore-this: ad1f82f22d1bf0e057f11c3508a81716
-] 
-
-[move embeddings into their own file; pull TPLT and PPLT into profinite.v
-robdockins@fastmail.fm**20140102234424
- Ignore-this: 3704996af47ae32415ba3e539d67cf5c
-] 
-
-[Show that PLT is cocartesian; rearrange proof that EMBED(true) is terminated
-robdockins@fastmail.fm**20140102213805
- Ignore-this: 3470df6910e7a3e4bda478c0c6ecea62
-] 
-
-[remove unnecessary "inh" hypothesis in the definition of Plotkin order; fixup the fallout
-robdockins@fastmail.fm**20140102213646
- Ignore-this: b6a5ad59296f938b377d71852120d48b
-] 
-
-[move proofs that empty and unit preorders are effective plotkin
-robdockins@fastmail.fm**20140102205530
- Ignore-this: 7324843510fd938d356aa82003c9ec68
-] 
-
-[make epi/mono/iso morphisms into categories
-robdockins@fastmail.fm**20131228082442
- Ignore-this: ee75a2b6eb1f3d6fa47f17d6734e5015
-] 
-
-[define the cocartesian and distributive categories
-robdockins@fastmail.fm**20131226001612
- Ignore-this: 11e9d8a88bef42bcb800b31d85d28d16
-] 
-
-[remove uses of maximally implict arguments
-robdockins@fastmail.fm**20131226001536
- Ignore-this: c0d93a5398aea58cbcc4fbbca3b59b17
-] 
-
-[fixpoints and binary sums for NOMINAL
-robdockins@fastmail.fm**20131121092931
- Ignore-this: 8a660dfe2ab16a8208ae559dcf2b7ed0
-] 
-
-[modify bilimit.v to use the general construction from cont_functors.v
-robdockins@fastmail.fm**20131120075848
- Ignore-this: 17ea36107ade1646eab5c99aec3561a9
-] 
-
-[generic fixpoint construction for categories with initial objects and directed colimits
-robdockins@fastmail.fm**20131119092522
- Ignore-this: 25674dff855a1cecdb4ee919f8bf3a5d
-] 
-
-[remove some irritating unit parameters, fix doc typos
-robdockins@fastmail.fm**20131118093204
- Ignore-this: 38342d58567d8a13471620d5b7c2b7d4
-] 
-
-[improvements to categories; complete some constructions in nominal
-robdockins@fastmail.fm**20131118085737
- Ignore-this: e58cb49a01d0210dabdb021250910adb
-] 
-
-[build fixes
-robdockins@fastmail.fm**20131113004305
- Ignore-this: 5abffcd1d6b44f816749c5e0cfd5b6e9
-] 
-
-[Documentation additions
-robdockins@fastmail.fm**20131113004254
- Ignore-this: 79a913d3a8652866f3fdc64891f6304d
-] 
-
-[lots of inline documentation additions
-robdockins@fastmail.fm**20131112192736
- Ignore-this: 6aa38112c10ceed3bf43e35dbda98312
-] 
-
-[update makefiles
-robdockins@fastmail.fm**20131112192706
- Ignore-this: d834beaa532cdf994cfa0a0b5a562e4f
-] 
-
-[continuous functors for binary sum and products
-robdockins@fastmail.fm**20131112192605
- Ignore-this: 61520e6e315df909465a02f854816366
-] 
-
-[add the category of nominal types
-robdockins@fastmail.fm**20131112192520
- Ignore-this: f0351c5eb0bdacdfe192a6863d9c0bc6
-] 
-
-[split the proof that expF is a continuous functor into a separate file; rearrange some defintions
-robdockins@fastmail.fm**20130924013328
- Ignore-this: 4eacee37bb6474d1bdfffe416b98b4c1
-] 
-
-[rearrange definitions of continuous functors. Prove enough plumbing to build the model: D = D->D
-robdockins@fastmail.fm**20130924002837
- Ignore-this: a66f9e8833601e244048b70e8bfaab96
-] 
-
-[show that the function space is a continuous functor; other junk
-robdockins@fastmail.fm**20130923060521
- Ignore-this: d8f406450688c633ebc1fe1eb0343c91
-] 
-
-[some name changes, other cosmetic fixes
-robdockins@fastmail.fm**20130909043234
- Ignore-this: cdd24d1c96a34fb3573c1806153df9fb
-] 
-
-[additional cosmetic changes and rearrangements
-robdockins@fastmail.fm**20130909020137
- Ignore-this: 77d28bc9452f6c93915194033118dab7
-] 
-
-[reorganize profinite code
-robdockins@fastmail.fm**20130909011437
- Ignore-this: 8511bf92ca6998ff8c69d5537624bdb8
-] 
-
-[cosmetic changes
-robdockins@fastmail.fm**20130908183909
- Ignore-this: e19039701e58fd26ca4eab79d7b49d14
-] 
-
-[complete the bilimit construction, show how to take fixpoints of continuous functors
-robdockins@fastmail.fm**20130908175228
- Ignore-this: 82feab8fdc0c944f13d91605c6a8e571
-] 
-
-[find a MUCH easier path to a bilimit construction
-robdockins@fastmail.fm**20130907012151
- Ignore-this: fcc72ad140b045ef37e4b03ad38a8fb0
-] 
-
-[lots of progress, mostly on defining bilimits
-robdockins@fastmail.fm**20130905204959
- Ignore-this: abf4bcf03a49fa009f9fb2200ee3abf2
-] 
-
-[start working on the theory of finite preorders, which form a basis for plokin orders
-robdockins@fastmail.fm**20130812054451
- Ignore-this: 5be36257a8fdf486bcc31f587d93c457
-] 
-
-[parameterize plotkin orders, build category PPLT
-robdockins@fastmail.fm**20130811063623
- Ignore-this: 3f273841bc72098acee0fd618627dbd5
-] 
-
-[complete the details showing PLT is cartesian closed
-robdockins@fastmail.fm**20130809230336
- Ignore-this: 13fd1b5a8172dd263cf655421f7584f7
-] 
-
-[add files missed in the first import
-robdockins@fastmail.fm**20130809080742
- Ignore-this: 6b59cce866a486d70559f7c80fe99053
-] 
-
-[initial import of development
-robdockins@fastmail.fm**20130809080409
- Ignore-this: 44cb5a0df2f1643d289f07dcd4227cbf
- First major steps toward a fully effective and usable formalized
- domain theory.  We formalize the plotkin preorders and show that
- they form a cartesian closed category.
-] 
diff --git a/pkgs/development/coq-modules/domains/default.nix b/pkgs/development/coq-modules/domains/default.nix
deleted file mode 100644
index 975260c839bd..000000000000
--- a/pkgs/development/coq-modules/domains/default.nix
+++ /dev/null
@@ -1,26 +0,0 @@
-{stdenv, fetchdarcs, coq}:
-
-stdenv.mkDerivation rec {
-
-  name = "coq-domains-${coq.coq-version}-${version}";
-  version = "ce1a9806";
-
-  src = fetchdarcs {
-    url = http://hub.darcs.net/rdockins/domains;
-    context = ./darcs_context;
-    sha256 = "0zdqiw08b453i8gdxwbk7nia2dv2r3pncmxsvgr0kva7f3dn1rnc";
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = with stdenv.lib; {
-    homepage = http://rwd.rdockins.name/domains/;
-    description = "A Coq library for domain theory";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/development/coq-modules/fiat/default.nix b/pkgs/development/coq-modules/fiat/default.nix
deleted file mode 100644
index e084497cbf81..000000000000
--- a/pkgs/development/coq-modules/fiat/default.nix
+++ /dev/null
@@ -1,41 +0,0 @@
-{stdenv, fetchurl, coq}:
-
-stdenv.mkDerivation rec {
-
-  name = "coq-fiat-${coq.coq-version}-${version}";
-  version = "20141031";
-
-  src = fetchurl {
-    url = "http://plv.csail.mit.edu/fiat/releases/fiat-${version}.tar.gz";
-    sha256 = "0c5jrcgbpdj0gfzg2q4naqw7frf0xxs1f451fnic6airvpaj0d55";
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  enableParallelBuilding = false;
-  doCheck = !stdenv.isi686;
-
-  unpackPhase = ''
-    mkdir fiat
-    cd fiat
-    tar xvzf ${src}
-  '';
-
-  buildPhase = "make -j$NIX_BUILD_CORES sources";
-  checkPhase = "make -j$NIX_BUILD_CORES examples";
-
-  installPhase = ''
-    COQLIB=$out/lib/coq/${coq.coq-version}/
-    mkdir -p $COQLIB/user-contrib/Fiat
-    cp -pR src/* $COQLIB/user-contrib/Fiat
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = http://plv.csail.mit.edu/fiat/;
-    description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index 683ab80b36bb..5faf8093b153 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -1,24 +1,12 @@
 { stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp
 , bignums ? null }:
 
-let param =
-  if stdenv.lib.versionAtLeast coq.coq-version "8.5"
-  then {
-    version = "3.3.0";
-    url = "https://gforge.inria.fr/frs/download.php/file/37077/interval-3.3.0.tar.gz";
-    sha256 = "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903";
-  } else {
-    version = "3.1.1";
-    url = "https://gforge.inria.fr/frs/download.php/file/36723/interval-3.1.1.tar.gz";
-    sha256 = "1sqsf075c7s98mwi291bhnrv5fgd7brrqrzx51747394hndlvfw3";
-  };
-in
-
 stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-interval-${param.version}";
+  name = "coq${coq.coq-version}-interval-3.3.0";
 
   src = fetchurl {
-    inherit (param) url sha256;
+    url = "https://gforge.inria.fr/frs/download.php/file/37077/interval-3.3.0.tar.gz";
+    sha256 = "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903";
   };
 
   nativeBuildInputs = [ which ];
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 48cb2c4d33fb..79bced9ad0ee 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -2,12 +2,6 @@
 
 let param =
   {
-    "8.4" =  {
-      version = "1.6.1";
-      url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
-      sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
-    };
-
     "8.5" =  {
       version = "1.6.1";
       url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix
index 35c23842158d..3b53a2831e8c 100644
--- a/pkgs/development/coq-modules/ssreflect/default.nix
+++ b/pkgs/development/coq-modules/ssreflect/default.nix
@@ -2,12 +2,6 @@
 
 let param =
   {
-    "8.4" =  {
-      version = "1.6.1";
-      url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
-      sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
-    };
-
     "8.5" =  {
       version = "1.6.1";
       url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix
deleted file mode 100644
index 2d30db5a80d4..000000000000
--- a/pkgs/development/coq-modules/tlc/default.nix
+++ /dev/null
@@ -1,38 +0,0 @@
-{stdenv, fetchsvn, coq}:
-
-stdenv.mkDerivation {
-
-  name = "coq-tlc-${coq.coq-version}";
-
-  src = fetchsvn {
-    url = svn://scm.gforge.inria.fr/svn/tlc/branches/v3.1;
-    rev = 240;
-    sha256 = "0mjnb6n9wzb13y2ix9cvd6irzd9d2gj8dcm2x71wgan0jcskxadm";
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  preConfigure = ''
-    patch Makefile <<EOF
-    105c105
-    < 	\$(COQC) \$<
-    ---
-    > 	\$(COQC) -R . Tlc \$<
-    EOF
-  '';
-
-  installPhase = ''
-    COQLIB=$out/lib/coq/${coq.coq-version}/
-    mkdir -p $COQLIB/user-contrib/Tlc
-    cp -p *.vo $COQLIB/user-contrib/Tlc
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = http://www.chargueraud.org/softs/tlc/;
-    description = "A general purpose Coq library that provides an alternative to Coq's standard library";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/development/coq-modules/unimath/default.nix b/pkgs/development/coq-modules/unimath/default.nix
deleted file mode 100644
index 8bd6cf5a84dd..000000000000
--- a/pkgs/development/coq-modules/unimath/default.nix
+++ /dev/null
@@ -1,26 +0,0 @@
-{stdenv, fetchgit, coq}:
-
-stdenv.mkDerivation rec {
-
-  name = "coq-unimath-${coq.coq-version}-${version}";
-  version = "a2714eca";
-
-  src = fetchgit {
-    url = git://github.com/UniMath/UniMath.git;
-    rev = "a2714eca29444a595cd280ea961ec33d17712009";
-    sha256 = "0v7dlyipr6bhwgp9v366nxdan018acafh13pachnjkgzzpsjnr7g";
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = with stdenv.lib; {
-    homepage = https://github.com/UniMath/UniMath;
-    description = "A formalization of a substantial body of mathematics using the univalent point of view";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/development/coq-modules/ynot/default.nix b/pkgs/development/coq-modules/ynot/default.nix
deleted file mode 100644
index d83e2c5c7909..000000000000
--- a/pkgs/development/coq-modules/ynot/default.nix
+++ /dev/null
@@ -1,32 +0,0 @@
-{stdenv, fetchgit, coq}:
-
-stdenv.mkDerivation rec {
-
-  name = "coq-ynot-${coq.coq-version}-${version}";
-  version = "ce1a9806";
-
-  src = fetchgit {
-    url = git://github.com/Ptival/ynot.git;
-    rev = "ce1a9806c26ffc6e7def41da50a9aac1433cb2f8";
-    sha256 = "1pcmcl5zamiimkcg1xvynxnfbv439y02vg1mnz79hqq9mnjyfnpw";
-  };
-
-  buildInputs = [ coq.ocaml coq.camlp5 ];
-  propagatedBuildInputs = [ coq ];
-
-  preBuild = "cd src";
-
-  installPhase = ''
-    COQLIB=$out/lib/coq/${coq.coq-version}/
-    mkdir -p $COQLIB/user-contrib/Ynot
-    cp -pR coq/*.vo $COQLIB/user-contrib/Ynot
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = http://ynot.cs.harvard.edu/;
-    description = "A library for writing and verifying imperative programs";
-    maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 0d72e719b79a..20ce40e10746 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -18811,39 +18811,6 @@ with pkgs;
   coq_8_7 = callPackage ../applications/science/logic/coq {
     version = "8.7.0";
   };
-  coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {};
-
-  mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
-    inherit callPackage;
-    coq = coq_8_4;
-    coqPackages = coqPackages_8_4;
-
-    contribs =
-      let contribs =
-        import ../development/coq-modules/contribs
-        contribs
-        callPackage { };
-      in
-        recurseIntoAttrs contribs;
-
-    bedrock = callPackage ../development/coq-modules/bedrock {};
-    coqExtLib = callPackage ../development/coq-modules/coq-ext-lib {};
-    coqeal = callPackage ../development/coq-modules/coqeal {};
-    coquelicot = callPackage ../development/coq-modules/coquelicot {};
-    domains = callPackage ../development/coq-modules/domains {};
-    fiat = callPackage ../development/coq-modules/fiat {};
-    fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
-    flocq = callPackage ../development/coq-modules/flocq {};
-    heq = callPackage ../development/coq-modules/heq {};
-    interval = callPackage ../development/coq-modules/interval {};
-    mathcomp = callPackage ../development/coq-modules/mathcomp {};
-    paco = callPackage ../development/coq-modules/paco {};
-    QuickChick = callPackage ../development/coq-modules/QuickChick {};
-    ssreflect = callPackage ../development/coq-modules/ssreflect {};
-    tlc = callPackage ../development/coq-modules/tlc {};
-    unimath = callPackage ../development/coq-modules/unimath {};
-    ynot = callPackage ../development/coq-modules/ynot {};
-  };
 
   mkCoqPackages = self: coq: let callPackage = newScope self; in rec {
     inherit callPackage coq;
@@ -18871,7 +18838,6 @@ with pkgs;
     equations = callPackage ../development/coq-modules/equations { };
   };
 
-  coqPackages_8_4 = mkCoqPackages_8_4 coqPackages_8_4;
   coqPackages_8_5 = mkCoqPackages coqPackages_8_5 coq_8_5;
   coqPackages_8_6 = mkCoqPackages coqPackages_8_6 coq_8_6;
   coqPackages_8_7 = mkCoqPackages coqPackages_8_7 coq_8_7;