Reloading sometimes flips order of sub-VCs, breaks existing proofs
Reloading (C-r
) in the IDE sometimes changes the order of VCs (cases of split_vc
,
inversion_arg_pr
, destruct_alg
, etc.), which invalidates existing proofs involving manual
transformations.
The reordering only happens occasionally and I have not yet found a reproducible case yet. Maybe somebody has an idea anyway of what goes wrong.
Edited by Benedikt Becker