summaryrefslogtreecommitdiff
path: root/plugins/extraction/json.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 18:33:25 +0100
commit1b92c226e563643da187b8614d5888dc4855eb43 (patch)
treec4c3d204b36468b58cb71050ba95f06b8dd7bc2e /plugins/extraction/json.ml
parent7c9b0a702976078b813e6493c1284af62a3f093c (diff)
Imported Upstream version 8.6
Diffstat (limited to 'plugins/extraction/json.ml')
-rw-r--r--plugins/extraction/json.ml8
1 files changed, 2 insertions, 6 deletions
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index df79c585..e43c47d0 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,8 +1,6 @@
open Pp
-open Errors
open Util
open Names
-open Nameops
open Globnames
open Table
open Miniml
@@ -18,9 +16,6 @@ let json_int i =
let json_bool b =
if b then str "true" else str "false"
-let json_null =
- str "null"
-
let json_global typ ref =
json_str (Common.pp_global typ ref)
@@ -147,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");