Coq 8.1 becomes trunk.

5 files changed, 0 insertions, 69 deletions

diff --git a/debian/coq-libs.dirs b/debian/coq-libs.dirs
deleted file mode 100644
index aadcf27a..00000000
--- a/debian/coq-libs.dirs
+++ /dev/null
@@ -1,2 +0,0 @@
-usr/share/doc/coq-libs
-usr/share/doc/coq
diff --git a/debian/coq-libs.doc-base b/debian/coq-libs.doc-base
deleted file mode 100644
index 1a62a262..00000000
--- a/debian/coq-libs.doc-base
+++ /dev/null
@@ -1,9 +0,0 @@
-Document: coq-library
-Title: The Coq Standard Library
-Author: The Coq Development Team
-Abstract: Standard Library documentation of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
-Section: Apps/Math
-
-Format: HTML
-Index: /usr/share/doc/coq-libs/html/index.html
-Files: /usr/share/doc/coq-libs/html/*.html
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
deleted file mode 100755
index ba55f3de..00000000
--- a/debian/patches/browser.dpatch
+++ /dev/null
@@ -1,19 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## browser.dpatch by Samuel Mimram <smimram@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Use the default Debian browser for help.
-
-@DPATCH@
-diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml
---- coq-8.0pl3+8.1alpha~/lib/options.ml	2005-12-26 20:07:21.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/lib/options.ml	2006-04-29 16:06:20.000000000 +0000
-@@ -117,7 +117,4 @@
-            "\" must contain exactly one placeholder \"%s\".")
-    else pre,post
-  with
--  Not_found ->
--   if Sys.os_type = "Win32"
--   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
--   else "netscape -remote \"OpenURL(", ")\""
-+  Not_found -> "/usr/bin/x-www-browser ", ""
diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
deleted file mode 100755
index fb618f56..00000000
--- a/debian/patches/coqdoc_stdlib.dpatch
+++ /dev/null
@@ -1,19 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## coqdoc_stdlib.dpatch by Samuel Mimram <smimram@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Add an option to coqdoc to be able to use a custom stdlib path in order
-## DP: to be able to build the documentation before coqdoc is installed.
-
-@DPATCH@
-diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile
---- coq-8.0pl3+8.1beta~/doc/Makefile	2006-06-16 13:02:33.000000000 +0000
-+++ coq-8.0pl3+8.1beta/doc/Makefile	2006-06-16 13:19:11.000000000 +0000
-@@ -216,6 +216,7 @@
- 	mkdir stdlib/html
- 	(cd stdlib/html;\
- 	 $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
-+	  --coqlib_path $(COQTOP) \
- 	  -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
- 	mv stdlib/html/index.html stdlib/index-body.html
- 
diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch
deleted file mode 100755
index b656a9bb..00000000
--- a/debian/patches/makefile.dpatch
+++ /dev/null
@@ -1,20 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## makefile.dpatch by Samuel Mimram <smimram@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Do not use ocamlopt to test grammar.cma, we don't want to use ocamlopt
-## DP: when compiling on non-native archs.
-
-@DPATCH@
-diff -urNad coq-8.0pl3+8.1alpha~/Makefile coq-8.0pl3+8.1alpha/Makefile
---- coq-8.0pl3+8.1alpha~/Makefile	2006-04-07 15:08:12.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/Makefile	2006-04-30 11:41:09.000000000 +0000
-@@ -1401,7 +1401,7 @@
- parsing/grammar.cma: $(GRAMMARCMO)
- 	$(SHOW)'Testing $@'
- 	@touch test.ml4
--	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
-+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
- 	@rm -f test-grammar test.*
- 	$(SHOW)'OCAMLC -a $@'   
- 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@