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:
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
new_lines is called to update the current position for errror reporting, so it might be something else I did...
Mamot.fr est une serveur Mastodon francophone, géré par La Quadrautre du Net.