Time Print foo doesn't print foo

[proofgeneral]

Time Print foo doesn't print foo

[Matafou]

This is linked to #19.

In Coq code, extraction outputs a "info" message, thus it is concatenated to Time info msg.

Whereas Print is a "notice" message,thus considered outdated by the info msg of Time.

It is too late to change coq_8.5 code and make Print display a "info" msg, moreover it should probably be the reverse: extraction should display a "notice". And this would not solve this issue but make it wider.

I will try to fix this with a workaround in pg, and we will take time to solve this properly in coq trunk.

[Matafou]

For information, I am about to fix this by two actions:

• pushing a small change in coq-8.5 making extraction use a non eager annotation (msg_notice).
• pushing a fix in pg which detects "Time" messages which are output just before the next prompt and do not consider them as "urgent" (but print them in response buffer anyway).

It is not perfect since some tag remain, but at least you can see the messages.

So now to see the fix you must update PG and Coq (8.5) to the very last git version.
P.