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
---
 tactics/auto.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

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