diff options
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | 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 be49aa351..8b7ee55bd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -993,8 +993,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 |