Permalink
Browse files

Dump references

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 1707245 commit 5b56756cfd2a3211e5b267d41be4a22679b78a4b @pirbo pirbo committed Aug 5, 2012
Showing with 2 additions and 0 deletions.
  1. +1 −0 plugins/extraction/table.ml
  2. +1 −0 tactics/auto.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
View
@@ -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

0 comments on commit 5b56756

Please sign in to comment.