diff --git a/pkgs/applications/science/logic/matita/130312.nix b/pkgs/applications/science/logic/matita/130312.nix
deleted file mode 100644
index 573b0ad7e4b5..000000000000
--- a/pkgs/applications/science/logic/matita/130312.nix
+++ /dev/null
@@ -1,65 +0,0 @@
-{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, ocaml_mysql, ocamlnet, ulex08, camlzip, ocaml_pcre, automake, autoconf }:
-
-let
-  version = "0.99.1pre130312";
-  pname = "matita";
-in
-
-stdenv.mkDerivation {
-  name = "${pname}-${version}";
-
-  src = fetchurl {
-    url = "http://matita.cs.unibo.it/sources/${pname}_130312.tar.gz";
-    sha256 = "13mjvvldv53dcdid6wmc6g8yn98xca26xq2rgq2jg700lqsni59s";
-  };
-
-  sourceRoot="${pname}-${version}";
-
-  unpackPhase = ''
-   mkdir $sourceRoot
-   tar -xvzf $src -C $sourceRoot
-   echo "source root is $sourceRoot"
-  '';
-
-  prePatch = ''
-   autoreconf -fvi
-  '';
-
-  buildInputs = [ocaml findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk ocaml_mysql ocamlnet ulex08 camlzip ocaml_pcre automake autoconf];
-
-  postPatch = ''
-    BASH=$(type -tp bash)
-    substituteInPlace components/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace matita/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace configure --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-content_pres.src --replace "ulex08" "ulex"
-    substituteInPlace components/content_pres/Makefile --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-grafite_parser.src --replace "ulex08" "ulex"
-    substituteInPlace components/grafite_parser/Makefile --replace "ulex08" "ulex"
-    substituteInPlace configure --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-getter.src --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
-  '';
-
-  patches = [ ./configure_130312.patch ];
-
-  preConfigure = ''
-    # Setup for findlib.
-    OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
-    RTDIR=$out/share/matita
-    export configureFlags="--with-runtime-dir=$RTDIR"
-  '';
-
-  postInstall = ''
-    mkdir -p $out/bin
-    ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin
-  '';
-
-  meta = {
-    homepage = http://matita.cs.unibo.it/;
-    description = "Matita is an experimental, interactive theorem prover";
-    license = stdenv.lib.licenses.gpl2Plus;
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-    broken = true;
-  };
-}
diff --git a/pkgs/applications/science/logic/matita/Makefile.patch b/pkgs/applications/science/logic/matita/Makefile.patch
deleted file mode 100644
index 64c9a13f2d07..000000000000
--- a/pkgs/applications/science/logic/matita/Makefile.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- matita-0.5.8/Makefile	2009-12-01 18:21:00.000000000 -0500
-+++ matita-0.5.8/Makefile	2010-09-16 10:33:59.665461260 -0400
-@@ -38,7 +38,7 @@
- uninstall: $(foreach d,$(SUBDIRS),rec@uninstall@$(d))
- 
- rec@%:
--	$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) DESTDIR=$(shell pwd)/$(DESTDIR)
-+	$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
- 
- # {{{ Distribution stuff
- 
diff --git a/pkgs/applications/science/logic/matita/configure.patch b/pkgs/applications/science/logic/matita/configure.patch
deleted file mode 100644
index 9a3bbbb13f52..000000000000
--- a/pkgs/applications/science/logic/matita/configure.patch
+++ /dev/null
@@ -1,36 +0,0 @@
---- zzz/matita-0.5.8/configure	2009-12-01 18:21:00.000000000 -0500
-+++ matita-0.5.8/configure	2010-09-07 19:57:29.732139550 -0400
-@@ -1895,6 +1895,7 @@
- # look for METAS dir
- 
- LIBSPATH="`pwd`/components"
-+OLDCAMLPATH="$OCAMLPATH"
- OCAMLPATH="$LIBSPATH/METAS"
- 
- # creating META.*
-@@ -1917,7 +1918,7 @@
- gdome2 \
- http \
- lablgtk2 \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- lablgtkmathview \
- mysql \
- netstring \
-@@ -1951,14 +1952,14 @@
- $FINDLIB_CREQUIRES \
- lablgtk2.glade \
- lablgtkmathview \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- helm-xmldiff \
- "
- for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
- do
-   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $r ocaml library" >&5
- $as_echo_n "checking for $r ocaml library... " >&6; }
--  if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-+  if OCAMLPATH=$OCAMLPATH:$OLDCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-     { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
- $as_echo "yes" >&6; }
-   else
diff --git a/pkgs/applications/science/logic/matita/configure_130312.patch b/pkgs/applications/science/logic/matita/configure_130312.patch
deleted file mode 100644
index 255feec566bf..000000000000
--- a/pkgs/applications/science/logic/matita/configure_130312.patch
+++ /dev/null
@@ -1,35 +0,0 @@
---- matita/configure     2011-11-22 06:04:17.000000000 -0500
-+++ matita/configure     2011-11-24 11:43:11.584847938 -0500
-@@ -1905,6 +1905,7 @@
- # look for METAS dir
- 
- LIBSPATH="`pwd`/components"
-+OLDCAMLPATH="$OCAMLPATH"
- OCAMLPATH="$LIBSPATH/METAS"
- 
- # creating META.*
-@@ -1927,7 +1928,7 @@
- gdome2 \
- http \
- lablgtk2 \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- mysql \
- netstring \
- ulex08 \
-@@ -1953,13 +1954,13 @@
- FINDLIB_REQUIRES="\
- $FINDLIB_CREQUIRES \
- lablgtk2.glade \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- "
- for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
- do
-   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $r ocaml library" >&5
- $as_echo_n "checking for $r ocaml library... " >&6; }
--  if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-+  if OCAMLPATH=$OCAMLPATH:$OLDCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-     { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
- $as_echo "yes" >&6; }
-   else
diff --git a/pkgs/applications/science/logic/matita/default.nix b/pkgs/applications/science/logic/matita/default.nix
deleted file mode 100644
index 5495f61bfd88..000000000000
--- a/pkgs/applications/science/logic/matita/default.nix
+++ /dev/null
@@ -1,52 +0,0 @@
-{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, lablgtkmathview, ocaml_mysql, ocaml_sqlite3, ocamlnet, ulex08, camlzip, ocaml_pcre }:
-
-let
-  version = "0.5.8";
-  pname = "matita";
-in
-
-stdenv.mkDerivation {
-  name = "${pname}-${version}";
-
-  src = fetchurl {
-    url = "http://matita.cs.unibo.it/FILES/${pname}-${version}.orig.tar.gz";
-    sha256 = "04sxklfak71khy1f07ks5c6163jbpxv6fmaw03fx8gwwlvpmzglh";
-  };
-
-  buildInputs = [ocaml findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre ];
-
-  postPatch = ''
-    BASH=$(type -tp bash)
-    substituteInPlace components/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace matita/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace configure --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-content_pres.src --replace "ulex08" "ulex"
-    substituteInPlace components/content_pres/Makefile --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-grafite_parser.src --replace "ulex08" "ulex"
-    substituteInPlace components/grafite_parser/Makefile --replace "ulex08" "ulex"
-    substituteInPlace configure --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-getter.src --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
-  '';
-
-  patches = [ ./configure.patch ./Makefile.patch ];
-
-  preConfigure = ''
-    # Setup for findlib.
-    OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
-    RTDIR=$out/share/matita
-    export configureFlags="--with-runtime-dir=$RTDIR"
-  '';
-
-  postInstall = ''
-    mkdir -p $out/bin
-    ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin
-  '';
-
-  meta = {
-    homepage = http://matita.cs.unibo.it/;
-    description = "Experimental, interactive theorem prover";
-    license = stdenv.lib.licenses.gpl2Plus;
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-  };
-}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 632b88c8012c..2da5edcd6646 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -21231,20 +21231,6 @@ with pkgs;
 
   ltl2ba = callPackage ../applications/science/logic/ltl2ba {};
 
-  #inherit (ocaml-ng.ocamlPackages_3_11_2) matita;
-
-  # Current version is 0.5.8. Official website says:
-
-  # Version 0.5.9, released on December 23, 2014, is an update of version 0.5.8
-  # to compile with the latter OCaml version and libraries.
-  # It is unsupported, but still used for teaching at the University of Bologna.
-
-  # It should allow us removing the dependency on OCaml 3.11 but I haven't been
-  # able to confirm because Matita depends on lablgtkmathview-0.7.2 which
-  # already reports as broken.
-
-  matita_130312 = lowPrio ocamlPackages.matita_130312;
-
   metis-prover = callPackage ../applications/science/logic/metis-prover { };
 
   mcrl2 = callPackage ../applications/science/logic/mcrl2 { };
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 4de581e2932d..5f6d6fc9bc1d 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -1051,12 +1051,6 @@ let
       camlp5 = camlp5_strict;
     };
 
-    matita = callPackage ../applications/science/logic/matita {
-      ulex08 = ulex08.override { camlp5 = camlp5_old_transitional; };
-    };
-
-    matita_130312 = callPackage ../applications/science/logic/matita/130312.nix { };
-
   };
     in (ocamlPackages.janeStreet // ocamlPackages);
     in lib.fix' (lib.extends overrides packageSet);