diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-05 18:16:31 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-05 18:22:38 +0100 |
commit | 32baedf7a3aebb96f7dd2c7d90a1aef40ed93792 (patch) | |
tree | d9d43648cb113f217581fea6fe248f4cf3805396 | |
parent | 35cc038e96395b0f4eaaeed3a5a48e6da2293f7e (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.
-rw-r--r-- | grammar/argextend.ml4 | 2 |
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< |