aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-05 18:16:31 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-05 18:22:38 +0100
commit32baedf7a3aebb96f7dd2c7d90a1aef40ed93792 (patch)
treed9d43648cb113f217581fea6fe248f4cf3805396 /grammar
parent35cc038e96395b0f4eaaeed3a5a48e6da2293f7e (diff)
Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".
The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation.
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 8def9537c..cb0f7d2d3 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -120,7 +120,7 @@ let make_possibly_empty_subentries loc s cl =
let make_act loc act pil =
let rec make = function
- | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
+ | [] -> <:expr< Pcoq.Gram.action (fun loc -> let loc = Compat.to_coqloc loc in ($act$ : 'a)) >>
| GramNonTerminal (_,t,_,Some p) :: tl ->
let p = Names.Id.to_string p in
<:expr<