refine goal order

Stream: lean4

[Jakob von Raumer]

refine and refine' seem to put goals in the wrong order in cases where all goals are in Prop and later goals depend on former goals. This deviates from the Lean3 behaviour and is quite inconvenient for porting... Has anybody else observed the same?