From 5e6d984197a986d511a4e54a38425499374e36c1 Mon Sep 17 00:00:00 2001
From: Helge Bahmann
Date: Mon, 14 Oct 2019 20:05:01 +0200
Subject: Fix coq#4741: Extract Constant/Inductive with JSON

Resolve by consulting is_custom/find_custom.
---
 plugins/extraction/json.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index fba6b7c780..912a20f389 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -16,7 +16,10 @@ let json_bool b =
   if b then str "true" else str "false"
 
 let json_global typ ref =
-  json_str (Common.pp_global typ ref)
+  if is_custom ref then
+    json_str (find_custom ref)
+  else
+    json_str (Common.pp_global typ ref)
 
 let json_id id =
   json_str (Id.to_string id)
-- 
cgit v1.2.3