3 files changed, 104 insertions, 0 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
index fa82f62e..1fbe17e1 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +1,3 @@
 coqdoc_stdlib
+failing_tests
+browser
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
new file mode 100755
index 00000000..ba55f3de
--- /dev/null
+++ b/debian/patches/browser.dpatch
@@ -0,0 +1,19 @@
+#! /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/failing_tests.dpatch b/debian/patches/failing_tests.dpatch
new file mode 100755
index 00000000..cc8429c8
--- /dev/null
+++ b/debian/patches/failing_tests.dpatch
@@ -0,0 +1,83 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## failing_tests.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Remove tests which don't succeed!
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1alpha~/test-suite/modules/mod_decl.v coq-8.0pl3+8.1alpha/test-suite/modules/mod_decl.v
+--- coq-8.0pl3+8.1alpha~/test-suite/modules/mod_decl.v	2005-12-21 23:50:17.000000000 +0000
++++ coq-8.0pl3+8.1alpha/test-suite/modules/mod_decl.v	1970-01-01 00:00:00.000000000 +0000
+@@ -1,49 +0,0 @@
+-Module Type SIG.
+-  Axiom A : Set.
+-End SIG.
+-
+-Module M0.
+-  Definition A : Set.
+-  exact nat.
+-  Qed.
+-End M0.
+-
+-Module M1 : SIG.
+-  Definition A := nat.
+-End M1.
+-
+-Module M2 <: SIG.
+-  Definition A := nat.
+-End M2.
+-
+-Module M3 := M0.
+-
+-Module M4 : SIG := M0.
+-
+-Module M5 <: SIG := M0.
+-
+-
+-Module F (X: SIG) := X.
+-
+-
+-Module Type T.
+-
+-  Module M0.
+-    Axiom A : Set.
+-  End M0.
+-  
+-  Declare Module M1: SIG.
+-  
+-  Declare Module M2 <: SIG.
+-    Definition A := nat.
+-  End M2.
+-  
+-  Module M3 := M0.
+-  
+-  Module M4 : SIG := M0.
+-  
+-  Module M5 <: SIG := M0.
+-
+-  Module M6 := F M0.
+-
+-End T.
+diff -urNad coq-8.0pl3+8.1alpha~/test-suite/output/Cases.out coq-8.0pl3+8.1alpha/test-suite/output/Cases.out
+--- coq-8.0pl3+8.1alpha~/test-suite/output/Cases.out	2005-12-21 23:50:17.000000000 +0000
++++ coq-8.0pl3+8.1alpha/test-suite/output/Cases.out	1970-01-01 00:00:00.000000000 +0000
+@@ -1,9 +0,0 @@
+-t_rect = 
+-fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
+-fix F (t : t) : P t :=
+-  match t as t0 return (P t0) with
+-  | k x x0 => f x0 (F x0)
+-  end
+-     : forall P : t -> Type,
+-       (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+-
+diff -urNad coq-8.0pl3+8.1alpha~/test-suite/output/Cases.v coq-8.0pl3+8.1alpha/test-suite/output/Cases.v
+--- coq-8.0pl3+8.1alpha~/test-suite/output/Cases.v	2005-12-21 23:50:17.000000000 +0000
++++ coq-8.0pl3+8.1alpha/test-suite/output/Cases.v	1970-01-01 00:00:00.000000000 +0000
+@@ -1,6 +0,0 @@
+-(* Cases with let-in in constructors types *)
+-
+-Inductive t : Set :=
+-    k : let x := t in x -> x.
+-
+-Print t_rect.