From d7f75509c290d871cb8cd8aa11a0be2923c9ef17 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 22 Sep 2015 19:44:47 +0200 Subject: Record the scope structure during unblocking. Instead of creating separate annotations for the local variables we call the Debug.add_lvar_scope and we construct a mapping from function id + scope id to scope information. --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 021dc512..33c4822d 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2227,7 +2227,7 @@ and elab_block_body env ctx sl = let (dcl, env') = elab_definition true env def in let loc = elab_loc (get_definitionloc def) in List.map (fun ((sto,id,ty,_) as d) -> - Debug.insert_local_declaration (-1) sto id ty loc;(* Dummy scope *) + Debug.insert_local_declaration sto id ty loc; {sdesc = Sdecl d; sloc = loc}) dcl @ elab_block_body env' ctx sl1 | s :: sl1 -> -- cgit