Fixing "change" and "fold" after convert_hyp/convert_concl moved to

new proof engine in e824d4293. Because of the expansion made by "fold"
and possibly by "change", checking the order of hypotheses is
necessary in general in "reduce". Before, it was done by side-effect
on reference "check", now it has to be explicit. To do for
optimization: flag each of the red_expr conversion strategy according
to whether they really need a check.

Also renamed the e_reduce family to e_change to emphasize that some
expansion can occur and that typing has to be rechecked.

This fixes recent failure of CoLoR (and probably Ergo).

0 files changed, 0 insertions, 0 deletions