Section My_Sec. GlobalArguments 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.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
