Patched for OCaml 3.08.1 + other minor things.

7 files changed, 74 insertions, 6 deletions

diff --git a/debian/TODO b/debian/TODO
new file mode 100644
index 00000000..783c4ca5
--- /dev/null
+++ b/debian/TODO
@@ -0,0 +1,6 @@
+* See if the -libs are arch-independant (I'm not sure but they should be). If
+  it's the case change them to Arch: all.
+
+* Move the coqide stuff from /usr/lib/coq/ide to /usr/share/coqide. The variable
+  lib_ide should be changed to do that.
+
diff --git a/debian/changelog b/debian/changelog
index c50dac73..87fe0318 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,7 +1,9 @@
 coq (8.0pl1-3) unstable; urgency=medium
 
+  * Small patch to be able to compile with ocaml 3.08.1.
   * Added a dependency to ocaml-base-nox when coq is compiled in bytecode.
-  * Added enhaced manpages.
+  * Added a menu for coqide.
+  * Enhanced the manpages.
   * Enhanced the short descriptions of the packages.
 
  -- Samuel Mimram <samuel.mimram@ens-lyon.org>  Tue, 17 Aug 2004 20:54:25 +0200
diff --git a/debian/control b/debian/control
index 2ca8c21b..3c6157d8 100644
--- a/debian/control
+++ b/debian/control
@@ -4,7 +4,7 @@ Priority: optional
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
 Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Jerome Marant <jerome@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <samuel.mimram@ens-lyon.org>
 Standards-Version: 3.6.1
-Build-Depends: debhelper (>= 4.0.0), ocaml-3.08, ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0)
+Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox-3.08, ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0)
 
 Package: coq
 Architecture: any
diff --git a/debian/coqide.menu b/debian/coqide.menu
new file mode 100644
index 00000000..00dc4139
--- /dev/null
+++ b/debian/coqide.menu
@@ -0,0 +1,4 @@
+?package(coqide):command="/usr/bin/coqide" \
+  icon="/usr/share/pixmaps/coq.xpm" \
+  needs="X11" \
+  section="Apps/Math" title="CoqIde"
diff --git a/debian/patches/00list b/debian/patches/00list
new file mode 100644
index 00000000..089b7a7b
--- /dev/null
+++ b/debian/patches/00list
@@ -0,0 +1 @@
+ocaml_3.08.1
diff --git a/debian/patches/ocaml_3.08.1.dpatch b/debian/patches/ocaml_3.08.1.dpatch
new file mode 100755
index 00000000..8327a7ae
--- /dev/null
+++ b/debian/patches/ocaml_3.08.1.dpatch
@@ -0,0 +1,55 @@
+#! /bin/sh -e
+## ocaml_3.08.1.dpatch by Michel Mauny <Michel.Mauny@inria.fr>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Add parenthesis to arguments of fun since without parenthesis is not accepted anymore by ocaml.
+
+if [ $# -lt 1 ]; then
+    echo "`basename $0`: script expects -patch|-unpatch as argument" >&2
+    exit 1
+fi
+
+[ -f debian/patches/00patch-opts ] && . debian/patches/00patch-opts
+patch_opts="${patch_opts:--f --no-backup-if-mismatch} ${2:+-d $2}"
+
+case "$1" in
+    -patch) patch -p1 ${patch_opts} < $0;;
+    -unpatch) patch -R -p1 ${patch_opts} < $0;;
+    *)
+        echo "`basename $0`: script expects -patch|-unpatch as argument" >&2
+        exit 1;;
+esac
+
+exit 0
+
+@DPATCH@
+diff -urNad /home/smimram/work/gnu/pkg-ocaml-maint/coq/trunk/coq-8.0pl1/contrib/funind/tacinv.ml4 coq-8.0pl1/contrib/funind/tacinv.ml4
+--- /home/smimram/work/gnu/pkg-ocaml-maint/coq/trunk/coq-8.0pl1/contrib/funind/tacinv.ml4	2004-02-10 17:22:14.000000000 +0100
++++ coq-8.0pl1/contrib/funind/tacinv.ml4	2004-08-20 14:40:56.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/debian/rules b/debian/rules
index 9f88bf6d..b48761d8 100755
--- a/debian/rules
+++ b/debian/rules
@@ -1,6 +1,8 @@
 #!/usr/bin/make -f
 # debian/rules for coq
 
+include /usr/share/dpatch/dpatch.make
+
 COQPREF=$(CURDIR)/debian/tmp
 ADDPREF=COQINSTALLPREFIX=$(COQPREF)
 
@@ -18,10 +20,9 @@ configure-stamp:
 	fi
 	touch configure-stamp
 
-build: configure-stamp build-stamp
+build: patch-stamp configure-stamp build-stamp
 build-stamp:
 	dh_testdir
-	touch test-suite/success/debian.v8
 	if grep -q BEST=opt config/Makefile; \
 	then \
 		($(MAKE) check \
@@ -38,7 +39,7 @@ build-stamp:
 	fi
 	touch build-stamp
 
-clean:
+clean: unpatch
 	dh_testdir
 	dh_testroot
 	rm -f build-stamp configure-stamp opt-stamp
@@ -72,7 +73,6 @@ install: build
 
 	dh_install --sourcedir=$(COQPREF)
 
-	#TODO: change lib_ide to /usr/share/coqide
 	cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt
 	if [ -e opt-stamp ]; then \
 		cp debian/coq/usr/share/man/man1/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \