diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /plugins/extraction/json.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
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)) ] |