Behaviour change of `apply` when creating evar. about math-comp HOT 4 CLOSED

That is intended, the behavior of 1.5 being a backward incompatible change. Yes, the fix was not quick...

from math-comp.

Just to be sure, the 1.5 -> 1.6 fix is the change you're speaking of ? I.e. that we have two incompatible changes in the picture: the one from 1.4 to 1.5 (when apply started to add goals for evars) and the one from 1.5 to 1.6 when this behaviour has been reverted ?

As a side note, is there a 1.5 -> 1.6 ChangeLog somewhere ?

from math-comp.

There is such a ChangeLog, shipped with the distribution here:
https://github.com/math-comp/math-comp/blob/master/etc/ChangeLog.
But it only mentions the issues with the library.
The corresponding (and so far more detailed) log for the tactic language is at the end of the manual:
https://github.com/math-comp/ssr-manual/blob/master/changes.tex
But it looks like we've not pushed content for versions >= 1.5 ...

Thanks for spotting that!

from math-comp.

There is no real changelog for the plugin because nothing really new happened.
Only two fixes, one for apply (that breaks wrt 1.5 and restores 1.4 behavior) and one for elim (that should accept more lemmas I believe).

from math-comp.