remove old versions

(Portage version: 2.1.3.15)

6 files changed, 6 insertions, 154 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index d16d0a10721c..1540334f880f 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,11 @@
 # ChangeLog for sci-mathematics/coq
 # Copyright 2000-2007 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.18 2007/10/20 15:37:29 aballier Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.19 2007/10/20 15:51:44 aballier Exp $
+
+  20 Oct 2007; Alexis Ballier <aballier@gentoo.org> -files/ocaml-3.07.patch,
+  -files/coq-8.0-byteflags.patch, -files/coq-8.0-ocaml-3.08.1.patch,
+  -coq-8.0-r1.ebuild:
+  remove old versions
 
 *coq-8.1_p2 (20 Oct 2007)
 
diff --git a/sci-mathematics/coq/coq-8.0-r1.ebuild b/sci-mathematics/coq/coq-8.0-r1.ebuild
deleted file mode 100644
index 2f70a919e20b..000000000000
--- a/sci-mathematics/coq/coq-8.0-r1.ebuild
+++ /dev/null
@@ -1,88 +0,0 @@
-# Copyright 1999-2007 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0-r1.ebuild,v 1.6 2007/07/02 15:26:46 peper Exp $
-
-inherit eutils
-
-IUSE="norealanalysis ide debug translator doc"
-
-RESTRICT="strip"
-
-MY_PV="8.0pl1"
-MY_P="${PN}-${MY_PV}"
-
-DESCRIPTION="Coq is a proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="ftp://ftp.inria.fr/INRIA/${PN}/V${MY_PV/_/}/${MY_P/_/}.tar.gz
-translator? ( ftp://ftp.inria.fr/INRIA/coq/V${MY_PV}/${MY_P}-translator.tar.gz )"
-
-LICENSE="LGPL-2.1"
-SLOT="0"
-KEYWORDS="~amd64 ppc sparc x86"
-
-DEPEND=">=dev-lang/ocaml-3.06
-ide? ( >=dev-ml/lablgtk-2.2.0 )"
-
-S="${WORKDIR}/${MY_P/_/}"
-
-src_unpack()
-{
-	unpack ${A}
-	cd ${S}
-	version=`ocamlc -v | grep 3.08.1`
-	if [ $? -eq 0 ]
-	then
-		epatch ${FILESDIR}/${P}-ocaml-3.08.1.patch
-	fi
-	epatch ${FILESDIR}/${P}-byteflags.patch
-}
-
-src_compile() {
-	local myconf="--prefix /usr \
-		--bindir /usr/bin \
-		--libdir /usr/lib/coq \
-		--mandir /usr/man \
-		--emacslib /usr/share/emacs/site-lisp \
-		--coqdocdir /usr/lib/coq/coqdoc"
-
-	use debug && myconf="--debug $myconf"
-	use norealanalysis && myconf="$myconf --reals"
-	use norealanalysis || myconf="$myconf --reals all"
-
-	if use ide; then
-		myconf="$myconf --coqide opt"
-	else
-		myconf="$myconf --coqide no"
-	fi
-
-	./configure $myconf || die
-
-	if use ide; then
-		labldir=/usr/lib/ocaml/lablgtk2
-		sed -i -e "s|BYTEFLAGS=|BYTEFLAGS=-I ${labldir} |" Makefile
-		sed -i -e "s|OPTFLAGS=|OPTFLAGS=-I ${labldir} |" Makefile
-		sed -i -e "s|COQIDEFLAGS=.*|COQIDEFLAGS=-thread -I ${labldir}|" Makefile
-		make world || die
-	else
-		make world
-	fi
-}
-
-src_install() {
-	make COQINSTALLPREFIX=${D} install || die
-	dodoc README CREDITS CHANGES LICENSE
-
-	if use translator; then
-		cd ${WORKDIR}/${MY_P}-translator
-		mv translate-v8 coq-translate-v8
-		dobin coq-translate-v8
-		if use doc; then
-			dodoc Translator.* syntax-v8.*
-		fi
-	fi
-
-	if use ide; then
-		insinto /usr/share/applnk/Edutainment/Mathematics
-		doins ${FILESDIR}/coqide.desktop
-	fi
-}
diff --git a/sci-mathematics/coq/files/coq-8.0-byteflags.patch b/sci-mathematics/coq/files/coq-8.0-byteflags.patch
deleted file mode 100644
index 7b4acf017689..000000000000
--- a/sci-mathematics/coq/files/coq-8.0-byteflags.patch
+++ /dev/null
@@ -1,20 +0,0 @@
---- Makefile.orig	2004-06-19 23:53:43.231742696 +0200
-+++ Makefile	2004-06-19 23:54:39.977116088 +0200
-@@ -346,7 +346,7 @@
- 
- $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
- 	$(SHOW)'COQMKTOP -o $@'	
--	$(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
-+	$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
- 
- $(COQTOP):
- 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
-@@ -570,7 +570,7 @@
- 
- $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma
- 	$(SHOW)'COQMKTOP -o $@'	
--	$(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
-+	$(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@
- 
- $(COQIDE):
- 	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
diff --git a/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch b/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
deleted file mode 100644
index 39f57e16521e..000000000000
--- a/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
+++ /dev/null
@@ -1,29 +0,0 @@
---- contrib/funind/tacinv.ml4.orig	2004-02-10 17:22:14.000000000 +0100
-+++ contrib/funind/tacinv.ml4	2004-08-20 13:29:59.000000000 +0200
-@@ -495,7 +495,7 @@
-        let metav = mknewmeta() in
-        let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
-        let newrec_call = substmeta rec_call in
--       let newlevar = List.map (fun ev,tev -> ev, substmeta tev) levar in
-+       let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in
-        let newabsc = Array.map substmeta absc in
-        newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms)
- 
-@@ -693,7 +693,7 @@
-  (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
-  let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
-  (* apply parameters immediately *)
-- let gl_abstr = applistc gl_abstr' (List.map (fun x,y,z -> x) (List.rev parms)) in
-+ let gl_abstr = applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in
- 
-  (* we apply args of the fix now, the parameters will be applied later *)
-  let princ_proof_applied_args = 
-@@ -790,7 +790,7 @@
-  in
-  let rec princ_replace_params params t = 
-   List.fold_left (
--   fun acc ev,nam,typ -> 
-+   fun acc (ev,nam,typ) -> 
-     mkLambda (Name (id_of_name nam) , typ, 
-     substitterm 0 ev (mkRel 1) (lift 0 acc)))
-    t (List.rev params) in
diff --git a/sci-mathematics/coq/files/digest-coq-8.0-r1 b/sci-mathematics/coq/files/digest-coq-8.0-r1
deleted file mode 100644
index ce6925235d8c..000000000000
--- a/sci-mathematics/coq/files/digest-coq-8.0-r1
+++ /dev/null
@@ -1,6 +0,0 @@
-MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233
-RMD160 dc241dcd596e5c667a4e8295eb44f23cbfef432e coq-8.0pl1-translator.tar.gz 233233
-SHA256 baea2c89f52c06062b3c38d3cd9367206dcbb7728a0315d1d2ce49524f4aa340 coq-8.0pl1-translator.tar.gz 233233
-MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613
-RMD160 e8437bc84e130757ae4bc46b832a95c0ea655da3 coq-8.0pl1.tar.gz 2272613
-SHA256 e90955b200b1bd64093eeebbad173d1228ea9d88aea0615a28de08782024be33 coq-8.0pl1.tar.gz 2272613
diff --git a/sci-mathematics/coq/files/ocaml-3.07.patch b/sci-mathematics/coq/files/ocaml-3.07.patch
deleted file mode 100644
index 707c51039b8a..000000000000
--- a/sci-mathematics/coq/files/ocaml-3.07.patch
+++ /dev/null
@@ -1,10 +0,0 @@
---- /root/tmp/coq-7.4/parsing/pcoq.ml4  2002-12-15 13:10:18.000000000 +0100
-+++ parsing/pcoq.ml4    2003-10-16 13:00:15.000000000 +0200
-@@ -108,6 +108,7 @@
-     type parsable = G.parsable
-     let parsable = G.parsable
-     let tokens = G.tokens
-+    let glexer = G.glexer
-     module Entry = G.Entry
-     module Unsafe = G.Unsafe
-