summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2015-06-17 15:36:29 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2015-10-13 17:25:14 +0200
commitfca0afda49e9411f25fc3d0b660b40a3dfd7d4bf (patch)
treee841344f766b319798852b1715837ac4f9923b29
parentab9ecfcac7b7c78e4ba84ddbfb36c86020f6b7e3 (diff)
Fix compilation with OCaml 4.02
-rw-r--r--debian/changelog6
-rw-r--r--debian/patches/0003-Fix-compilation-with-OCaml-4.02.patch22
-rw-r--r--debian/patches/series1
3 files changed, 29 insertions, 0 deletions
diff --git a/debian/changelog b/debian/changelog
index 8deffbc0..d0a9cf27 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,9 @@
+coq (8.4pl4dfsg-2) UNRELEASED; urgency=medium
+
+ * Fix compilation with OCaml 4.02
+
+ -- Stéphane Glondu <glondu@debian.org> Fri, 19 Jun 2015 19:54:30 +0200
+
coq (8.4pl4dfsg-1) unstable; urgency=medium
* New upstream release (Closes: #755953)
diff --git a/debian/patches/0003-Fix-compilation-with-OCaml-4.02.patch b/debian/patches/0003-Fix-compilation-with-OCaml-4.02.patch
new file mode 100644
index 00000000..3e5c5e6d
--- /dev/null
+++ b/debian/patches/0003-Fix-compilation-with-OCaml-4.02.patch
@@ -0,0 +1,22 @@
+From: Stephane Glondu <steph@glondu.net>
+Date: Wed, 17 Jun 2015 15:36:10 +0200
+Subject: Fix compilation with OCaml 4.02
+
+---
+ kernel/univ.ml | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/kernel/univ.ml b/kernel/univ.ml
+index 822f6ca..53342dd 100644
+--- a/kernel/univ.ml
++++ b/kernel/univ.ml
+@@ -226,7 +226,7 @@ let reprleq g arcu =
+
+
+ (* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *)
+-(* between u v = {w|u<=w<=v, w canonical} *)
++(* between u v = (w|u<=w<=v, w canonical) *)
+ (* between is the most costly operation *)
+
+ let between g arcu arcv =
+--
diff --git a/debian/patches/series b/debian/patches/series
index a2649778..3404177e 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
0002-Disable-micromega-tests-on-Hurd.patch
+0003-Fix-compilation-with-OCaml-4.02.patch