Incompatibilities with 8.15.1 ?

[JonasOberhauser]

It seems some lemmas are incompatible with 8.15.1, or something is wrong on my end.

The problems are in HahnMinPath and HahnWf.

the problem in HahnWf seems to be related to a mismatch between the internal name of the binder (y) and what is shown on screen (y0). It can be fixed like this:

    rename y into y'. (* not necessary, but makes sure that the names stay the same *)
    apply In_split in IN; desf.
    eapply H with (y := l1 ++ l2); ins. (* was y0:= *)
      by rewrite !app_length; simpl; lia.

However it's strange that the names are not the same and could point to the problem being in my installation.