From 3c87a1cb2ae89284c70c6b9333a88a06fc4d060f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 7 Apr 2014 20:57:42 -0400
Subject: Add a regression test for bug 3001

---
 test-suite/bugs/closed/3001.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/3001.v

diff --git a/test-suite/bugs/closed/3001.v b/test-suite/bugs/closed/3001.v
new file mode 100644
index 0000000000..6e56555499
--- /dev/null
+++ b/test-suite/bugs/closed/3001.v
@@ -0,0 +1,21 @@
+Definition my_fun (n:nat) := n.
+
+Section My_Sec.
+  Global Arguments my_fun x : rename.
+End My_Sec.
+
+(* The following code suffices to trigger it, on my system:
+
+    Definition my_fun (n:nat) := n.
+
+    Section My_Sec.
+    Global Arguments my_fun x : rename.
+    End My_Sec.
+
+The `Global Arguments` declaration succeeds fine, but the `End My_Sec` fails, with `Anomaly: dirpath_prefix: empty dirpath. Please report.`
+
+If `Global` is removed, or if no arguments are renamed, then everything works as expected.
+
+If other declarations go between the `Global Arguments` and the `End My_Sec`, then the other declarations work normally, but the `End My_Sec` still fails.
+
+Previously reported at https://github.com/HoTT/coq/issues/24 .  Occurs in both 8.4 and current trunk. *)
-- 
cgit v1.2.3