summaryrefslogtreecommitdiff
path: root/debian/patches
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
commit6b61b68d5822575015583047e1d266b8257e35d5 (patch)
tree3bf0a2c20b8732a96238c5bd85409c4e618ea6ef /debian/patches
parente669490d0d5e6ed4bb45c895194791f01d038637 (diff)
New upstream release: 8.0pl2.debian/8.0pl2-1
Diffstat (limited to 'debian/patches')
-rw-r--r--debian/patches/00list1
-rwxr-xr-xdebian/patches/ocaml_3.08.1.dpatch55
2 files changed, 0 insertions, 56 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
index 089b7a7b..e69de29b 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +0,0 @@
-ocaml_3.08.1
diff --git a/debian/patches/ocaml_3.08.1.dpatch b/debian/patches/ocaml_3.08.1.dpatch
deleted file mode 100755
index 8327a7ae..00000000
--- a/debian/patches/ocaml_3.08.1.dpatch
+++ /dev/null
@@ -1,55 +0,0 @@
-#! /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