From 3a6650a4adcef0bf8c8afb316c227b4aa21d560e Mon Sep 17 00:00:00 2001
From: pboutill
Date: Sun, 5 Aug 2012 23:13:04 +0000
Subject: Dump references in Reset

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15677 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 011818c15e..46fdeb5326 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1466,6 +1466,22 @@ let vernac_back n =
 
 let vernac_reset_name id =
   try
+    let globalized =
+      try
+	let gr = Smartlocate.global_with_alias (Ident id) in
+	Dumpglob.add_glob (fst id) gr;
+	true
+      with _ -> false in
+
+    if not globalized then begin
+       try begin match Lib.find_opening_node (snd id) with
+          | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id)
+              (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
+          (* Might be nice to implement module cases, too.... *)
+          | _ -> ()
+       end with UserError _ -> ()
+    end;
+
     if Backtrack.is_active () then
       (Backtrack.reset_name id; try_print_subgoals ())
     else
-- 
cgit v1.2.3