From 5b56756cfd2a3211e5b267d41be4a22679b78a4b Mon Sep 17 00:00:00 2001
From: pboutill
Date: Sun, 5 Aug 2012 23:13:10 +0000
Subject: Dump references

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/table.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 62ce89896a..886a19e94f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -842,6 +842,7 @@ let extract_constant_inline inline r ids s =
 let extract_inductive r s l optstr =
   check_inside_section ();
   let g = Smartlocate.global_with_alias r in
+  Dumpglob.add_glob (loc_of_reference r) g;
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
-- 
cgit v1.2.3