diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-17 11:58:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-17 11:58:21 +0200 |
| commit | e5f8038f82c8a444afcfb7333a4c690b005fcff6 (patch) | |
| tree | 51e7e5ac47aba0ff26d1d6ed3da84f1d6a1183df /plugins/extraction/json.ml | |
| parent | 67c713cab69a54f5347c987aa0076aeddd1bceef (diff) | |
Fix bug #5023: JSON extraction doesn't generate "for xxx".
Diffstat (limited to 'plugins/extraction/json.ml')
| -rw-r--r-- | plugins/extraction/json.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 8874afef3..e43c47d05 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -142,7 +142,8 @@ let rec json_expr env = function ("what", json_str "fix:item"); ("name", json_id fi); ("body", json_function env' ti) - ]) (Array.map2 (fun a b -> a,b) ids' defs))) + ]) (Array.map2 (fun a b -> a,b) ids' defs))); + ("for", json_int i); ] | MLexn s -> json_dict [ ("what", json_str "expr:exception"); |