coq icon indicating copy to clipboard operation
coq copied to clipboard

Published 20 hours ago • verified publisher icon HoTT

Globally renaming arguments within section causes "Anomaly: dirpath_prefix: empty dirpath."

Open peterlefanulumsdaine opened this issue 11 years ago • 4 comments

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.

(Working over HoTT/coq@b07e5d72278f62b40ba338deadd55fd634fc80fc, i.e. current stable branch. I haven’t tested this in the main coq trunk since I’m having problems building that, but I will do so as soon as I can.)

peterlefanulumsdaine avatar Mar 12 '13 06:03 peterlefanulumsdaine

This code triggers the bug in v8.4. You should probably report it on http://www.lix.polytechnique.fr/coq/bugs/.

JasonGross avatar Mar 12 '13 08:03 JasonGross

Thanks — ok, reported there!

peterlefanulumsdaine avatar Mar 12 '13 14:03 peterlefanulumsdaine

Fixed

gares avatar Apr 18 '13 13:04 gares

This is fixed in polyproj. Can we (@peterlefanulumsdaine or @mattam82) close this issue?

JasonGross avatar Apr 08 '14 01:04 JasonGross