remove old

(Portage version: 2.2.0_alpha43/cvs/Linux x86_64)

9 files changed, 7 insertions, 545 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index 4f6f364c96ad..26a32e8996eb 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,12 @@
 # ChangeLog for sci-mathematics/coq
 # Copyright 1999-2011 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.64 2011/06/03 15:02:14 ranger Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.65 2011/07/06 18:41:39 aballier Exp $
+
+  06 Jul 2011; Alexis Ballier <aballier@gentoo.org> -coq-8.2_p1-r1.ebuild,
+  -coq-8.2_p2.ebuild, -files/coq-8.2_p2-camlp5-6-compat.patch,
+  -files/coq-8.2_p2-make-3.82.patch, -coq-8.3.ebuild,
+  -files/coq-8.3-camlp5-6-compat.patch, -files/coq-8.3-make-3.82-compat.patch:
+  remove old
 
   03 Jun 2011; Brent Baude <ranger@gentoo.org> coq-8.3_p1.ebuild:
   Marking coq-8.3_p1 ppc for bug 355539
diff --git a/sci-mathematics/coq/coq-8.2_p1-r1.ebuild b/sci-mathematics/coq/coq-8.2_p1-r1.ebuild
deleted file mode 100644
index 64370466da52..000000000000
--- a/sci-mathematics/coq/coq-8.2_p1-r1.ebuild
+++ /dev/null
@@ -1,76 +0,0 @@
-# Copyright 1999-2011 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.2_p1-r1.ebuild,v 1.10 2011/02/27 18:12:02 armin76 Exp $
-
-EAPI="2"
-
-inherit eutils multilib
-
-MY_PV="${PV/_p/pl}"
-MY_P="${PN}-${MY_PV}"
-
-DESCRIPTION="Coq is a proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="http://coq.inria.fr/distrib/V${MY_PV}/files/${MY_P}.tar.gz"
-
-LICENSE="LGPL-2.1"
-SLOT="0"
-KEYWORDS="amd64 ppc x86"
-IUSE="norealanalysis gtk debug +ocamlopt doc"
-
-RDEPEND=">=dev-lang/ocaml-3.10[ocamlopt?]
-	>=dev-ml/camlp5-5.09[ocamlopt?]
-	gtk? ( >=dev-ml/lablgtk-2.10.1[ocamlopt?] )"
-DEPEND="${RDEPEND}
-	doc? (
-		media-libs/netpbm[png,zlib]
-		virtual/latex-base
-		dev-tex/hevea
-		dev-tex/xcolor
-		|| ( dev-texlive/texlive-pictures app-text/ptex )
-		|| ( dev-texlive/texlive-mathextra app-text/ptex )
-		|| ( dev-texlive/texlive-latexextra app-text/ptex )
-		)"
-
-S="${WORKDIR}/${MY_P}"
-
-src_configure() {
-	ocaml_lib=`ocamlc -where`
-	local myconf="--prefix /usr
-		--bindir /usr/bin
-		--libdir /usr/$(get_libdir)/coq
-		--mandir /usr/share/man
-		--emacslib /usr/share/emacs/site-lisp
-		--coqdocdir /usr/$(get_libdir)/coq/coqdoc
-		--docdir /usr/share/doc/${PF}
-		--camlp5dir ${ocaml_lib}/camlp5
-		--lablgtkdir ${ocaml_lib}/lablgtk2"
-
-	use debug && myconf="--debug $myconf"
-	use norealanalysis && myconf="$myconf --reals no"
-	use norealanalysis || myconf="$myconf --reals all"
-	use doc || myconf="$myconf --with-doc no"
-
-	if use gtk; then
-		use ocamlopt && myconf="$myconf --coqide opt"
-		use ocamlopt || myconf="$myconf --coqide byte"
-	else
-		myconf="$myconf --coqide no"
-	fi
-	use ocamlopt || myconf="$myconf -byte-only"
-	use ocamlopt && myconf="$myconf --opt"
-
-	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
-	./configure $myconf || die "configure failed"
-}
-
-src_compile() {
-	emake STRIP="true" -j1 || die "make failed"
-}
-
-src_install() {
-	emake STRIP="true" COQINSTALLPREFIX="${D}" install || die
-	dodoc README CREDITS CHANGES
-
-	use gtk && domenu "${FILESDIR}/coqide.desktop"
-}
diff --git a/sci-mathematics/coq/coq-8.2_p2.ebuild b/sci-mathematics/coq/coq-8.2_p2.ebuild
deleted file mode 100644
index 6f45b693949c..000000000000
--- a/sci-mathematics/coq/coq-8.2_p2.ebuild
+++ /dev/null
@@ -1,80 +0,0 @@
-# Copyright 1999-2011 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.2_p2.ebuild,v 1.6 2011/02/27 18:12:02 armin76 Exp $
-
-EAPI=2
-inherit eutils multilib
-
-MY_PV=${PV/_p/pl}
-MY_P=${PN}-${MY_PV}
-
-DESCRIPTION="Coq is a proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="http://coq.inria.fr/distrib/V${MY_PV}/files/${MY_P}.tar.gz"
-
-LICENSE="LGPL-2.1"
-SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
-IUSE="+realanalysis gtk debug +ocamlopt doc"
-
-RDEPEND=">=dev-lang/ocaml-3.10[ocamlopt?]
-	>=dev-ml/camlp5-5.09[ocamlopt?]
-	gtk? ( >=dev-ml/lablgtk-2.10.1[ocamlopt?] )"
-DEPEND="${RDEPEND}
-	doc? (
-		media-libs/netpbm[png,zlib]
-		virtual/latex-base
-		dev-tex/hevea
-		dev-tex/xcolor
-		|| ( dev-texlive/texlive-pictures app-text/ptex )
-		|| ( dev-texlive/texlive-mathextra app-text/ptex )
-		|| ( dev-texlive/texlive-latexextra app-text/ptex )
-		)"
-
-S=${WORKDIR}/${MY_P}
-
-src_prepare() {
-	epatch "${FILESDIR}"/${P}-make-3.82.patch
-	epatch "${FILESDIR}"/${P}-camlp5-6-compat.patch
-}
-
-src_configure() {
-	ocaml_lib=`ocamlc -where`
-	local myconf="--prefix /usr
-		--bindir /usr/bin
-		--libdir /usr/$(get_libdir)/coq
-		--mandir /usr/share/man
-		--emacslib /usr/share/emacs/site-lisp
-		--coqdocdir /usr/$(get_libdir)/coq/coqdoc
-		--docdir /usr/share/doc/${PF}
-		--camlp5dir ${ocaml_lib}/camlp5
-		--lablgtkdir ${ocaml_lib}/lablgtk2"
-
-	use debug && myconf="--debug $myconf"
-	use realanalysis || myconf="$myconf --reals no"
-	use realanalysis && myconf="$myconf --reals all"
-	use doc || myconf="$myconf --with-doc no"
-
-	if use gtk; then
-		use ocamlopt && myconf="$myconf --coqide opt"
-		use ocamlopt || myconf="$myconf --coqide byte"
-	else
-		myconf="$myconf --coqide no"
-	fi
-	use ocamlopt || myconf="$myconf -byte-only"
-	use ocamlopt && myconf="$myconf --opt"
-
-	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
-	./configure $myconf || die "configure failed"
-}
-
-src_compile() {
-	emake STRIP="true" -j1 || die "make failed"
-}
-
-src_install() {
-	emake STRIP="true" COQINSTALLPREFIX="${D}" install || die
-	dodoc README CREDITS CHANGES
-
-	use gtk && domenu "${FILESDIR}/coqide.desktop"
-}
diff --git a/sci-mathematics/coq/coq-8.3.ebuild b/sci-mathematics/coq/coq-8.3.ebuild
deleted file mode 100644
index 41a1df0408c4..000000000000
--- a/sci-mathematics/coq/coq-8.3.ebuild
+++ /dev/null
@@ -1,79 +0,0 @@
-# Copyright 1999-2011 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3.ebuild,v 1.3 2011/02/27 18:12:02 armin76 Exp $
-
-EAPI="2"
-
-inherit eutils multilib
-
-DESCRIPTION="Coq is a proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="http://${PN}.inria.fr/V${PV}/files/${P}.tar.gz"
-
-LICENSE="LGPL-2.1"
-SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
-IUSE="gtk debug +ocamlopt doc"
-
-RDEPEND=">=dev-lang/ocaml-3.10[ocamlopt?]
-	>=dev-ml/camlp5-5.09[ocamlopt?]
-	gtk? ( >=dev-ml/lablgtk-2.10.1[ocamlopt?] )"
-DEPEND="${RDEPEND}
-	doc? (
-		media-libs/netpbm[png,zlib]
-		virtual/latex-base
-		dev-tex/hevea
-		dev-tex/xcolor
-		|| ( dev-texlive/texlive-pictures app-text/ptex )
-		|| ( dev-texlive/texlive-mathextra app-text/ptex )
-		|| ( dev-texlive/texlive-latexextra app-text/ptex )
-		)"
-
-src_prepare() {
-	# From upstream CVS, remove on next patchlevel:
-	epatch "${FILESDIR}/${P}-camlp5-6-compat.patch"
-	epatch "${FILESDIR}/${P}-make-3.82-compat.patch"
-	# configure has an error at line 640 leading to closing a string
-	# to early in the generated coq_config.ml. Here is a wild sed :)
-	# It replaces \"$LABLGTKLIB\" by $LABLGTKLIB
-	sed -i "s/\\\\\"\\\$LABLGTKLIB\\\\\"/\\\$LABLGTKLIB/" configure
-}
-
-src_configure() {
-	ocaml_lib=`ocamlc -where`
-	local myconf="--prefix /usr
-		--bindir /usr/bin
-		--libdir /usr/$(get_libdir)/coq
-		--mandir /usr/share/man
-		--emacslib /usr/share/emacs/site-lisp
-		--coqdocdir /usr/$(get_libdir)/coq/coqdoc
-		--docdir /usr/share/doc/${PF}
-		--camlp5dir ${ocaml_lib}/camlp5
-		--lablgtkdir ${ocaml_lib}/lablgtk2"
-
-	use debug && myconf="--debug $myconf"
-	use doc || myconf="$myconf --with-doc no"
-
-	if use gtk; then
-		use ocamlopt && myconf="$myconf --coqide opt"
-		use ocamlopt || myconf="$myconf --coqide byte"
-	else
-		myconf="$myconf --coqide no"
-	fi
-	use ocamlopt || myconf="$myconf -byte-only"
-	use ocamlopt && myconf="$myconf --opt"
-
-	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
-	./configure $myconf || die "configure failed"
-}
-
-src_compile() {
-	emake STRIP="true" -j1 || die "make failed"
-}
-
-src_install() {
-	emake STRIP="true" COQINSTALLPREFIX="${D}" install || die
-	dodoc README CREDITS CHANGES
-
-	use gtk && domenu "${FILESDIR}/coqide.desktop"
-}
diff --git a/sci-mathematics/coq/files/coq-8.2_p2-camlp5-6-compat.patch b/sci-mathematics/coq/files/coq-8.2_p2-camlp5-6-compat.patch
deleted file mode 100644
index 3734f75ffc15..000000000000
--- a/sci-mathematics/coq/files/coq-8.2_p2-camlp5-6-compat.patch
+++ /dev/null
@@ -1,131 +0,0 @@
-diff -Naurp coq-8.2pl2/lib/compat.ml4 a/lib/compat.ml4
---- coq-8.2pl2/lib/compat.ml4	2007-09-15 10:35:59.000000000 +0000
-+++ a/lib/compat.ml4	2011-02-17 07:30:00.000000000 +0000
-@@ -69,3 +69,16 @@ let join_loc = M.join_loc
- type token = M.token
- type lexer = M.lexer
- let using = M.using
-+
-+IFDEF CAMLP5_6_00 THEN
-+
-+let slist0sep x y = Gramext.Slist0sep (x, y, false)
-+let slist1sep x y = Gramext.Slist1sep (x, y, false)
-+
-+ELSE
-+
-+let slist0sep x y = Gramext.Slist0sep (x, y)
-+let slist1sep x y = Gramext.Slist1sep (x, y)
-+
-+END
-+
-diff -Naurp coq-8.2pl2/parsing/pcoq.ml4 a/parsing/pcoq.ml4
---- coq-8.2pl2/parsing/pcoq.ml4	2009-04-07 18:19:05.000000000 +0000
-+++ a/parsing/pcoq.ml4	2011-02-17 07:30:45.000000000 +0000
-@@ -159,6 +159,11 @@ module Gram =
-       errorlabstrm "Pcoq.delete_rule" (str "GDELETE_RULE forbidden.")
-   end
- 
-+IFDEF CAMLP5_6_02_1 THEN
-+let entry_print x = Gram.Entry.print !Pp_control.std_ft x
-+ELSE
-+let entry_print = Gram.Entry.print
-+END
- 
- let camlp4_verbosity silent f x =
-   let a = !Gramext.warning_verbose in
-@@ -746,9 +751,9 @@ let rec symbol_of_production assoc from
-     | ETConstrList (typ',[]) ->
-         Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ'))
-     | ETConstrList (typ',tkl) ->
--        Gramext.Slist1sep
--          (symbol_of_production assoc from forpat (ETConstr typ'),
--           Gramext.srules
-+        Compat.slist1sep
-+          (symbol_of_production assoc from forpat (ETConstr typ'))
-+           (Gramext.srules
-              [List.map (fun x -> Gramext.Stoken x) tkl,
-               List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
-                 (Gramext.action (fun loc -> ()))])
-diff -Naurp coq-8.2pl2/parsing/pcoq.mli a/parsing/pcoq.mli
---- coq-8.2pl2/parsing/pcoq.mli	2009-01-14 11:36:32.000000000 +0000
-+++ a/parsing/pcoq.mli	2011-02-17 07:30:52.000000000 +0000
-@@ -24,6 +24,8 @@ val lexer : Compat.lexer
- 
- module Gram : Grammar.S with type te = Compat.token
- 
-+val entry_print : 'a Gram.Entry.e -> unit
-+
- (* The superclass of all grammar entries *)
- type grammar_object
- 
-diff -Naurp coq-8.2pl2/parsing/q_util.ml4 a/parsing/q_util.ml4
---- coq-8.2pl2/parsing/q_util.ml4	2008-08-06 10:30:35.000000000 +0000
-+++ a/parsing/q_util.ml4	2011-02-17 07:31:00.000000000 +0000
-@@ -82,7 +82,7 @@ let modifiers e =
- <:expr<  Gramext.srules
-     [([], Gramext.action(fun _loc -> []));
-      ([Gramext.Stoken ("", "(");
--       Gramext.Slist1sep ($e$, Gramext.Stoken ("", ","));
-+       Compat.slist1sep ($e$) (Gramext.Stoken ("", ","));
-        Gramext.Stoken ("", ")")],
-       Gramext.action (fun _ l _ _loc -> l))]
-  >>
-@@ -96,7 +96,7 @@ let rec interp_entry_name loc s sep =
-                    String.sub s (l-9) 9 = "_list_sep" then
-     let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in
-     let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in
--    List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >>
-+    List1ArgType t, <:expr< Compat.slist1sep $g$ $sep$ >>
-   else if l > 5 & String.sub s (l-5) 5 = "_list" then
-     let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in
-     List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
-diff -Naurp coq-8.2pl2/toplevel/metasyntax.ml a/toplevel/metasyntax.ml
---- coq-8.2pl2/toplevel/metasyntax.ml	2010-03-23 22:34:38.000000000 +0000
-+++ a/toplevel/metasyntax.ml	2011-02-17 07:30:35.000000000 +0000
-@@ -100,33 +100,33 @@ let add_tactic_notation (n,prods,e) =
- let print_grammar = function
-   | "constr" | "operconstr" | "binder_constr" ->
-       msgnl (str "Entry constr is");
--      Gram.Entry.print Pcoq.Constr.constr;
-+      entry_print Pcoq.Constr.constr;
-       msgnl (str "and lconstr is");
--      Gram.Entry.print Pcoq.Constr.lconstr;
-+      entry_print Pcoq.Constr.lconstr;
-       msgnl (str "where binder_constr is");
--      Gram.Entry.print Pcoq.Constr.binder_constr;
-+      entry_print Pcoq.Constr.binder_constr;
-       msgnl (str "and operconstr is");
--      Gram.Entry.print Pcoq.Constr.operconstr;
-+      entry_print Pcoq.Constr.operconstr;
-   | "pattern" ->
--      Gram.Entry.print Pcoq.Constr.pattern
-+      entry_print Pcoq.Constr.pattern
-   | "tactic" -> 
-       msgnl (str "Entry tactic_expr is");
--      Gram.Entry.print Pcoq.Tactic.tactic_expr;
-+      entry_print Pcoq.Tactic.tactic_expr;
-       msgnl (str "Entry binder_tactic is");
--      Gram.Entry.print Pcoq.Tactic.binder_tactic;
-+      entry_print Pcoq.Tactic.binder_tactic;
-       msgnl (str "Entry simple_tactic is");
--      Gram.Entry.print Pcoq.Tactic.simple_tactic;
-+      entry_print Pcoq.Tactic.simple_tactic;
-   | "vernac" -> 
-       msgnl (str "Entry vernac is");
--      Gram.Entry.print Pcoq.Vernac_.vernac;
-+      entry_print Pcoq.Vernac_.vernac;
-       msgnl (str "Entry command is");
--      Gram.Entry.print Pcoq.Vernac_.command;
-+      entry_print Pcoq.Vernac_.command;
-       msgnl (str "Entry syntax is");
--      Gram.Entry.print Pcoq.Vernac_.syntax;
-+      entry_print Pcoq.Vernac_.syntax;
-       msgnl (str "Entry gallina is");
--      Gram.Entry.print Pcoq.Vernac_.gallina;
-+      entry_print Pcoq.Vernac_.gallina;
-       msgnl (str "Entry gallina_ext is");
--      Gram.Entry.print Pcoq.Vernac_.gallina_ext;
-+      entry_print Pcoq.Vernac_.gallina_ext;
-   | _ -> error "Unknown or unprintable grammar entry."
- 
- (**********************************************************************)
diff --git a/sci-mathematics/coq/files/coq-8.2_p2-make-3.82.patch b/sci-mathematics/coq/files/coq-8.2_p2-make-3.82.patch
deleted file mode 100644
index af46977b932c..000000000000
--- a/sci-mathematics/coq/files/coq-8.2_p2-make-3.82.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-http://bugs.gentoo.org/341187
-
---- configure
-+++ configure
-@@ -327,6 +327,8 @@
-   case $MAKEVERSION in
-     "GNU Make 3.81") 
-       echo "You have GNU Make 3.81. Good!";;
-+    "GNU Make 3.82")
-+      echo "You have GNU Make 3.82. Good!";;
-     *)
-       OK="no"
-       if [ -x ./make ]; then
diff --git a/sci-mathematics/coq/files/coq-8.3-camlp5-6-compat.patch b/sci-mathematics/coq/files/coq-8.3-camlp5-6-compat.patch
deleted file mode 100644
index 50ae78340dbc..000000000000
--- a/sci-mathematics/coq/files/coq-8.3-camlp5-6-compat.patch
+++ /dev/null
@@ -1,77 +0,0 @@
-From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Date: Tue, 16 Nov 2010 20:25:56 +0000 (+0000)
-Subject: Support for camlp5 6.02.0 (Closes: #2432)
-X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=501c9cb6ff7c903974123284fe795cdcaab8f300
-
-Support for camlp5 6.02.0 (Closes: #2432)
-
-git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13641 85f007b7-540e-0410-9357-904b9bb8a0f7
----
-
-diff --git a/lib/compat.ml4 b/lib/compat.ml4
-index 9b6bb19..a77c2bc 100644
---- a/lib/compat.ml4
-+++ b/lib/compat.ml4
-@@ -65,3 +65,15 @@ let unloc = M.unloc
- let join_loc = M.join_loc
- type token = M.token
- type lexer = M.lexer
-+
-+IFDEF CAMLP5_6_00 THEN
-+
-+let slist0sep x y = Gramext.Slist0sep (x, y, false)
-+let slist1sep x y = Gramext.Slist1sep (x, y, false)
-+
-+ELSE
-+
-+let slist0sep x y = Gramext.Slist0sep (x, y)
-+let slist1sep x y = Gramext.Slist1sep (x, y)
-+
-+END
-diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
-index 4719e6d..5d37f4a 100644
---- a/parsing/pcoq.ml4
-+++ b/parsing/pcoq.ml4
-@@ -631,16 +631,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
-     | ETConstrList (typ',[]) ->
-         Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
-     | ETConstrList (typ',tkl) ->
--        Gramext.Slist1sep
--          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
--	   make_sep_rules tkl)
-+        Compat.slist1sep
-+          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
-+          (make_sep_rules tkl)
-     | ETBinderList (false,[]) ->
-         Gramext.Slist1
- 	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
-     | ETBinderList (false,tkl) ->
--        Gramext.Slist1sep
--	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
--	   make_sep_rules tkl)
-+        Compat.slist1sep
-+          (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
-+          (make_sep_rules tkl)
-     | _ ->
-     match interp_constr_prod_entry_key assoc from forpat typ with
-       | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
-@@ -654,16 +654,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
- let rec symbol_of_prod_entry_key = function
-   | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
-   | Alist1sep (s,sep) ->
--      Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
-+      Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
-   | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
-   | Alist0sep (s,sep) ->
--      Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
-+      Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
-   | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
-   | Amodifiers s ->
-        Gramext.srules
-         [([], Gramext.action(fun _loc -> []));
-          ([Gramext.Stoken ("", "(");
--           Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ","));
-+           Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ","));
-            Gramext.Stoken ("", ")")],
- 	   Gramext.action (fun _ l _ _loc -> l))]
-   | Aself -> Gramext.Sself
diff --git a/sci-mathematics/coq/files/coq-8.3-make-3.82-compat.patch b/sci-mathematics/coq/files/coq-8.3-make-3.82-compat.patch
deleted file mode 100644
index 5176aa33ec8a..000000000000
--- a/sci-mathematics/coq/files/coq-8.3-make-3.82-compat.patch
+++ /dev/null
@@ -1,84 +0,0 @@
-From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Date: Tue, 19 Oct 2010 13:22:08 +0000 (+0000)
-Subject: Fix mixed implicit and normal rules
-X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=86eb08bad450dd3fa77b11e4a34d2f493ab80d85
-
-Fix mixed implicit and normal rules
-
-This fixes build with GNU Make 3.82. See threads:
-
-  https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
-  http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
-
-git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13566 85f007b7-540e-0410-9357-904b9bb8a0f7
----
-
-diff --git a/Makefile b/Makefile
-index b1edc01..ea73c51 100644
---- a/Makefile
-+++ b/Makefile
-@@ -160,9 +160,19 @@ else
- stage1 $(STAGE1_TARGETS) : always
- 	$(call stage-template,1)
- 
-+ifneq (,$(STAGE1_IMPLICITS))
-+$(STAGE1_IMPLICITS) : always
-+	$(call stage-template,1)
-+endif
-+
- stage2 $(STAGE2_TARGETS) : stage1
- 	$(call stage-template,2)
- 
-+ifneq (,$(STAGE2_IMPLICITS))
-+$(STAGE2_IMPLICITS) : stage1
-+	$(call stage-template,2)
-+endif
-+
- # Nota:
- # - world is one of the targets in $(STAGE2_TARGETS), hence launching
- # "make" or "make world" leads to recursion into stage1 then stage2
-diff --git a/Makefile.common b/Makefile.common
-index cc38980..46bf217 100644
---- a/Makefile.common
-+++ b/Makefile.common
-@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y")
- 
- SOURCEDOCDIR=dev/source-doc
- 
--CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
-+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
- 
- ### Targets forwarded by Makefile to a specific stage:
- 
-@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
- STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
-   $(GENFILES) \
-   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
--  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
-+  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
-+
-+STAGE1_IMPLICITS:=
- 
- ifdef CM_STAGE1
-- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
-+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
- endif
- 
- ## Enumeration of targets that require being done at stage2
-@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
-   printers debug initplugins plugins \
-   world install coqide coqide-files coq coqlib \
-   coqlight states check init theories theories-light \
--  $(DOC_TARGETS) $(VO_TARGETS) validate \
--  %.vo %.glob states/% install-% %.ml4-preprocessed \
-+  $(DOC_TARGETS) $(VO_TARGETS) validate
-+
-+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
-   $(DOC_TARGET_PATTERNS)
- 
- ifndef CM_STAGE1
-- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
-+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
- endif
- 
- 
diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml
index 948b4b1f508b..76cdd62b5c99 100644
--- a/sci-mathematics/coq/metadata.xml
+++ b/sci-mathematics/coq/metadata.xml
@@ -16,8 +16,4 @@
   Constructions" extended by a modular development system for
   theories.
 </longdescription>
-<use>
-  <flag name='norealanalysis'>Do not build real analysis modules (faster compilation)</flag>
-  <flag name='realanalysis'>Build real analysis modules (slower compilation)</flag>
-</use>
 </pkgmetadata>