diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-14 02:51:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-14 11:14:09 +0100 |
| commit | 4331c26d60d7109f49d082113d40b896ea6a1fae (patch) | |
| tree | 67913708f9e267c80724f5fb34efd77c2d8454e7 | |
| parent | 5872768853f8c78187a3daaa89f09e674c90fa07 (diff) | |
Fix an ordering issue that was causing a test to fail in bytecode
| -rw-r--r-- | debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch | 31 | ||||
| -rw-r--r-- | debian/patches/series | 1 |
2 files changed, 32 insertions, 0 deletions
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 00000000..3307023d --- /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@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 1d411110..41965593 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 |