[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, experimental/master, updated. debian/8.4_beta+dfsg-1-4-g144b082
Stephane Glondu
steph at glondu.net
Sat Jan 14 10:59:14 UTC 2012
The following commit has been merged in the experimental/master branch:
commit 4331c26d60d7109f49d082113d40b896ea6a1fae
Author: Stephane Glondu <steph at glondu.net>
Date: Sat Jan 14 02:51:40 2012 +0100
Fix an ordering issue that was causing a test to fail in bytecode
diff --git a/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
new file mode 100644
index 0000000..3307023
--- /dev/null
+++ b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
@@ -0,0 +1,31 @@
+From: Stephane Glondu <steph at glondu.net>
+Date: Sat, 14 Jan 2012 01:24:30 +0100
+Subject: coq_micromega.ml: fix order of recursive calls to rconstant
+
+Some tests were failing on architectures without native code because
+the evaluation order of arguments in a function call is not the same
+on bytecode, leading to different behaviours for the psatzl tactic.
+---
+ plugins/micromega/coq_micromega.ml | 8 ++++++--
+ 1 files changed, 6 insertions(+), 2 deletions(-)
+
+diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
+index 1ad49bb..543ab1b 100644
+--- a/plugins/micromega/coq_micromega.ml
++++ b/plugins/micromega/coq_micromega.ml
+@@ -991,8 +991,12 @@ struct
+ else raise ParseError
+ | App(op,args) ->
+ begin
+- try
+- (assoc_const op rconst_assoc) (rconstant args.(0)) (rconstant args.(1))
++ try
++ (* the evaluation order is important in the following *)
++ let f = assoc_const op rconst_assoc in
++ let a = rconstant args.(0) in
++ let b = rconstant args.(1) in
++ f a b
+ with
+ ParseError ->
+ match op with
+--
diff --git a/debian/patches/series b/debian/patches/series
index 1d41111..4196559 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1 +1,2 @@
0001-Add-distclean-back-to-test-suite-Makefile.patch
+0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
--
coq packaging
More information about the Pkg-ocaml-maint-commits
mailing list