diff options
Diffstat (limited to 'plugins/extraction/json.ml')
| -rw-r--r-- | plugins/extraction/json.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index f88d29e9ed..fba6b7c780 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,7 +1,6 @@ open Pp open Util open Names -open Globnames open Table open Miniml open Mlutil @@ -200,10 +199,10 @@ and json_function env t = let json_ind ip pl cv = json_dict [ ("what", json_str "decl:ind"); - ("name", json_global Type (IndRef ip)); + ("name", json_global Type (GlobRef.IndRef ip)); ("argnames", json_list (List.map json_id pl)); ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [ - ("name", json_global Cons (ConstructRef (ip, idx+1))); + ("name", json_global Cons (GlobRef.ConstructRef (ip, idx+1))); ("argtypes", json_list (List.map (json_type pl) c)) ]) cv)) ] |