@lyxia Hi!
I wanted to use the “begin details” environment now that coq.8.12 is finally out, and it turns out it is broken.

I am not sure, but I think this is due to your patch here:
github.com/coq/coq/commit/41a1

I think the issue lies in the Lexing.new_line lexbuf; you have introduced. Can you explain to me why you did this? To see if I can just propose a PR where it is removed without breaking anything else

Follow

@lthms
new_lines is called to update the current position for errror reporting, so it might be something else I did...

@lyxia my understanding is that you added a `nl` at the wrong place during your refactoring

@lthms
Oh I see. I misunderstood the syntax of begin details, thought it was a standalone tag like the others. Sorry about that.

@lyxia no worries. I am just not sure the call to new_lines is necessary at all, since it is probably already embedded inside details_body.

@lthms
That's the third thing I broke with that patch... I should work on some tests around that part...

@lyxia I am adding a test for details right now! At least this one should be fine

Sign in to participate in the conversation
La Quadrature du Net - Mastodon - Media Fédéré

Mamot.fr est une serveur Mastodon francophone, géré par La Quadrautre du Net.