summaryrefslogtreecommitdiff
path: root/debian/patches/ocaml_3.08.1.dpatch
diff options
context:
space:
mode:
Diffstat (limited to 'debian/patches/ocaml_3.08.1.dpatch')
-rwxr-xr-xdebian/patches/ocaml_3.08.1.dpatch55
1 files changed, 55 insertions, 0 deletions
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