coq-elpi The interp implementation of coq.env.current-section-path uses a synterp-specific API

The interp implementation of coq.env.current-section-path uses a synterp-specific API

Open rlepigre opened this issue 4 months ago • 0 comments

This used to also be the case for coq.env.current-path, but we fixed it in https://github.com/LPCIC/coq-elpi/pull/605.

There is no available Coq API that would let us correctly implement coq.env.current-section-path at interp it seems (see here).

CC @Janno.

Feb 29 '24 23:02 rlepigre