Add missing `Proof.` to sealing proofs
This helps async proof checking (see iris/iris!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.' ```
Showing
- theories/algebra/big_op.v 3 additions, 3 deletionstheories/algebra/big_op.v
- theories/algebra/ofe.v 1 addition, 1 deletiontheories/algebra/ofe.v
- theories/base_logic/lib/fancy_updates.v 1 addition, 1 deletiontheories/base_logic/lib/fancy_updates.v
- theories/base_logic/lib/gen_heap.v 3 additions, 3 deletionstheories/base_logic/lib/gen_heap.v
- theories/base_logic/lib/invariants.v 1 addition, 1 deletiontheories/base_logic/lib/invariants.v
- theories/base_logic/lib/own.v 1 addition, 1 deletiontheories/base_logic/lib/own.v
- theories/base_logic/lib/proph_map.v 1 addition, 1 deletiontheories/base_logic/lib/proph_map.v
- theories/base_logic/upred.v 15 additions, 15 deletionstheories/base_logic/upred.v
- theories/bi/big_op.v 1 addition, 1 deletiontheories/bi/big_op.v
- theories/bi/lib/atomic.v 1 addition, 1 deletiontheories/bi/lib/atomic.v
- theories/bi/monpred.v 19 additions, 19 deletionstheories/bi/monpred.v
- theories/program_logic/total_weakestpre.v 1 addition, 1 deletiontheories/program_logic/total_weakestpre.v
- theories/program_logic/weakestpre.v 1 addition, 1 deletiontheories/program_logic/weakestpre.v
- theories/si_logic/siprop.v 8 additions, 8 deletionstheories/si_logic/siprop.v
Loading
Please register or sign in to comment