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 +
 tactics/auto.ml             | 1 +
 2 files changed, 2 insertions(+)

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
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 161fe66fc0..20c3f7680d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -864,6 +864,7 @@ let interp_hints h =
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
+	Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
         list_tabulate (fun i -> let c = (ind,i+1) in
 			 None, true, PathHints [ConstructRef c], mkConstruct c)
 	  (nconstructors ind) in
-- 
cgit v1.2.3