Sounds interesting! Is it enough for you to know if the current document contains an error sentence (i.e. a sentence marked in red)? Because this is easy to get although we have not documented the API so much :(
There is a pending issue on this: https://github.com/jscoq/jscoq/issues/216
As of today there is little structure on Coq documents, indeed most of you can do is to query a particular sentence for information, in this case for example you could ask indeed for goals or for success status kind of easily.
But indeed see the discussion @Shachar Itzhaky pointed
Last updated: Nov 29 2023 at 04:01 UTC