Pierre Courtieu

Results 266 comments of Pierre Courtieu

Experiments to fix the goals not showing on errors.

Thanks @ejgallego that makes sense to look there. But my intuition is that printing errors first is correct (error messages are more urgent?). Maybe the problem is that the prompt...

Experiments to fix the goals not showing on errors.

We need this ordering of appearance: WARNINGS/ERRORS GOAL PROMPT Which suggest IIUC that ERRORS should be flushed first, BUT ALSO that the prompt should not be printed on the error...

Experiments to fix the goals not showing on errors.

OK I will submit a bug report. Of course flushing is per formatter, my question is: **why on earth should the prompt be on the error formatter** anyways??

Experiments to fix the goals not showing on errors.

@aa755 can you try https://github.com/Matafou/coq/tree/fix-prompt-err-17753 and see if the bug is fixed?

Do not offer to save (temporary) buffers without associated files

Thanks for the ping. Let us merge this right now.

Fix compilation issues and remove uses of old advice facility

LGTM. Thanks Stefan.

Fix #18332 (specialize does not support evars in the instantiated args)

hmm the failed test is precisely documented as a change of behaviour introduced by the recoding of specialize. So this patch re-instates the original behaviour as a side effect of...

Fix #18332 (specialize does not support evars in the instantiated args)

Actually thinking a bit more about it I am not convinced by the remark cited above: ``` specialize IHn with (1 := eq_refl). ``` Giving `eq_refl` here means giving a...

Fix #18332 (specialize does not support evars in the instantiated args)

Ready for review and full ci. No documentation is needed. I put a test in `test-suite/success/specialize` But I could also put it in `test-suite/bugs/bug_xxx.v` if someone recommends it.

Fix #18332 (specialize does not support evars in the instantiated args)

I see you point @ppedrot. Ultimately `specialize` would create goals like `refine` but no shelved evars. The problem is that based on my experiment in LibHyps I don't think it...