diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-04-05 10:52:45 -0400 |
|---|---|---|
| committer |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 12:09:03 +0200 |
| commit | fb8c4b8903e82b36ebcf28dfe18282fb05a93d4f (patch) | |
| tree | 303d0ef85d919bd87cdd59cd9551ff3ef17b09e2 /plugins/extraction | |
| parent | b23edffbb4c0f57a5988c3ae218987f15e215097 (diff) | |
JSON extraction: construct full names (dot-separated) in pp_global
This is important to disambiguate identical names from different modules.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 094d91d20..97f856944 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -600,7 +600,7 @@ let pp_global k r = let rls = List.rev ls in (* for what come next it's easier this way *) match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) - | JSON -> unquote s (* no modular JSON extraction... *) + | JSON -> dottify (List.map unquote rls) | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) |