l4v
l4v copied to clipboard
MCS: synchronise proof directories with master
Several proof directories on the rt branch had diverged from master in unexpected ways. This commit manually brings them back in sync.
The specific directories are access-control, bisim, dpolicy, drefine, and infoflow.
Good to bring them in sync again. A lot of these look like wrong indentation got fixed on the MCS side. No problem reverting this here, but we should probably add a todo to fix it in master instead, so it gets carried over in the next merge.
I actually thought it was the other way around, the indentation was fixed on master and had been previously accidentally reverted on MCS.
Good to bring them in sync again. A lot of these look like wrong indentation got fixed on the MCS side. No problem reverting this here, but we should probably add a todo to fix it in master instead, so it gets carried over in the next merge.
I actually thought it was the other way around, the indentation was fixed on master and had been previously accidentally reverted on MCS.
Entirely possible :-) I thought I saw an example where the indent is now wrong, but I might just have been wrong about that or it's mixed. In any case, the flow should be from master to rt, so no point trying to fix indent in the rt branch.