Suppression du répertoire distrib: il fait désormais partie du projet coq-dev-tools sur GForge

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8943 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 0 insertions, 157 deletions

diff --git a/distrib/RH/coq.spec b/distrib/RH/coq.spec
deleted file mode 100644
index 30a1e577dd..0000000000
--- a/distrib/RH/coq.spec
+++ /dev/null
@@ -1,52 +0,0 @@
-Name: coq
-Version: 8.0
-Release: 2
-Summary: The Coq Proof Assistant
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
-Icon: petit-coq.gif
-BuildRoot: /var/tmp/coq
-
-%description
-Coq is a proof assistant which: 
-  - allows to handle calculus assertions, 
-  - check mechanically proofs of these assertions, 
-  - helps to find formal proofs, 
-  - extracts a certified program from the constructive proof
-    of its formal specification, 
-
-Requires: ocaml >= 3.06
-
-%define debug_package %{nil}
-                                                                               
-%prep
-%setup
-
-%build
-./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-   -emacslib %{_datadir}/emacs/site-lisp \
-   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
-   -opt -reals all -coqide no
-make coq
-
-
-%clean
-rm -rf %{buildroot}
-make clean
-
-%install
-rm -rf %{buildroot}
-make -e COQINSTALLPREFIX=%{buildroot} install-coq
-
-%define __spec_install_post /usr/lib/rpm/brp-compress
-
-%files
-%defattr(-,root,root)
-%{_bindir}/*
-%{_libdir}/coq
-%{_mandir}/man1/*
-%{_datadir}/emacs/site-lisp/*
-%{_datadir}/texmf/tex/latex/misc/*
diff --git a/distrib/RH/coq_ext_for_pcoq.spec b/distrib/RH/coq_ext_for_pcoq.spec
deleted file mode 100644
index 954be7239d..0000000000
--- a/distrib/RH/coq_ext_for_pcoq.spec
+++ /dev/null
@@ -1,45 +0,0 @@
-Name: coq_ext_for_pcoq
-Version: 8.0
-Release: 2
-Summary: The Coq Extension for Pcoq
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
-Icon: petit-coq.gif
-Requires: coq = 8.0
-BuildRoot: /var/tmp/pcoq
-
-%description
-The Coq Extension for Pcoq provides all facilities to interface Coq with
-Pcoq
-
-%define debug_package %{nil}
-
-%prep
-%setup -n coq-8.0
-
-%build
-./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-   -emacslib %{_datadir}/emacs/site-lisp \
-   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
-   -opt -reals all -coqide no
-make pcoq
-
-%clean
-rm -rf %{buildroot}
-make clean
-
-%install
-rm -rf %{buildroot}
-make -e COQINSTALLPREFIX=%{buildroot} install-pcoq
-
-%define __spec_install_post /usr/lib/rpm/brp-compress
-
-%files
-%defattr(-,root,root)
-%{_bindir}/*
-%{_libdir}/coq/contrib/interface
-%{_mandir}/man1/*
-
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
deleted file mode 100644
index 3fd25c4231..0000000000
--- a/distrib/RH/coqide.spec
+++ /dev/null
@@ -1,56 +0,0 @@
-Name: coqide
-Version: 8.0
-Release: 2
-Summary: The Coq Integrated Development Interface
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
-Icon: petit-coq.gif
-Requires: coq = 8.0
-BuildRoot: /var/tmp/coqide
-
-%description
-The Coq Integrated Development Interface is a graphical interface for the 
-Coq proof assistant 
-
-%define debug_package %{nil}
-
-%prep
-%setup -n coq-8.0
-
-%build
-./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-   -emacslib %{_datadir}/emacs/site-lisp \
-   -coqdocdir %{_datadir}/texmf/tex/latex/misc -opt -reals all
-make coqide
-
-%clean
-rm -rf %{buildroot}
-make clean
-
-%install
-rm -rf %{buildroot}
-make -e COQINSTALLPREFIX=%{buildroot} install-coqide
-
-# menu entry
-mkdir -p %{buildroot}%{_menudir}
-cat > %{buildroot}%{_menudir}/CoqIDE << _EOF_
-?package(CoqIDE): \
- command="%{_bindir}/coqide" \
-# icon="coqide.png" \ TODO add an icon
- longtitle="The Coq Integrated Development Interface" \
- needs="x11" \
- section="Applications/Sciences/Mathematics" \
- title="CoqIDE" \
- startup_notify="yes"
-_EOF_
-
-%define __spec_install_post /usr/lib/rpm/brp-compress
-
-%files
-%defattr(-,root,root)
-%{_menudir}/CoqIDE
-%{_bindir}/*
-%{_libdir}/coq/ide
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
deleted file mode 100644
index 103d4a880a..0000000000
--- a/distrib/RH/do_build
+++ /dev/null
@@ -1,2 +0,0 @@
-./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make coq       # Use native coq to compile theories
diff --git a/distrib/RH/do_build_pcoq b/distrib/RH/do_build_pcoq
deleted file mode 100755
index 0477d001bd..0000000000
--- a/distrib/RH/do_build_pcoq
+++ /dev/null
@@ -1,2 +0,0 @@
-./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make pcoq      # Use native coq to compile theories