diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-17 18:09:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-17 18:09:28 +0200 |
| commit | 1929b52db6bc282c60a1a3aa39ba87307c68bf78 (patch) | |
| tree | 57a6c7632dec646afb3ab6a1a9519eb313e805ac /plugins/extraction | |
| parent | 05ad4f49ac2203dd64dfec79a1fc62ee52115724 (diff) | |
| parent | 34b1813b5adf1df556e0d8a05bde0ec58152f610 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'plugins/extraction')
| -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"); |