aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 6839ac9f..6c941a1f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2226,7 +2226,9 @@ and elab_block_body env ctx sl =
| DEFINITION def :: sl1 ->
let (dcl, env') = elab_definition true env def in
let loc = elab_loc (get_definitionloc def) in
- List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl
+ List.map (fun ((sto,id,ty,_) as d) ->
+ Debug.insert_local_declaration sto id ty loc;
+ {sdesc = Sdecl d; sloc = loc}) dcl
@ elab_block_body env' ctx sl1
| s :: sl1 ->
let s' = elab_stmt env ctx s in