blob: 3307023d5675d46605c11dce54ed9dd3adeb0658 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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
--
|
