Skip to content

Add missing `Proof.` to sealing proofs to help async proof checking

Paolo G. Giarrusso requested to merge Blaisorblade/iris:add-missing-proof into master

This helps async proof checking (see !406 (comment 46759)).

Done with

gsed -i 's/seal \(.*\)\. by eexists. Qed./seal \1. Proof. by eexists. Qed./' \
  $(find theories/ -name '*.v')

And checked by inspecting the output of:

git grep '\bseal\b'|fgrep -v 'Proof. by eexists. Qed.'
Edited by Paolo G. Giarrusso

Merge request reports