From c514a452ff3ba2980ddd5a4b2f795af361b3c101 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 29 Apr 2006 16:32:35 +0000 Subject: Last modifications before upload. --- debian/patches/00list | 2 + debian/patches/browser.dpatch | 19 +++++++++ debian/patches/failing_tests.dpatch | 83 +++++++++++++++++++++++++++++++++++++ 3 files changed, 104 insertions(+) create mode 100755 debian/patches/browser.dpatch create mode 100755 debian/patches/failing_tests.dpatch (limited to 'debian/patches') 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 +## +## 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 +## +## 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. -- cgit v1.2.3