do not eta-expand when sealing
Showing
- theories/algebra/ofe.v 2 additions, 1 deletiontheories/algebra/ofe.v
- theories/base_logic/lib/fancy_updates.v 5 additions, 4 deletionstheories/base_logic/lib/fancy_updates.v
- theories/base_logic/lib/gen_heap.v 2 additions, 1 deletiontheories/base_logic/lib/gen_heap.v
- theories/base_logic/lib/invariants.v 2 additions, 2 deletionstheories/base_logic/lib/invariants.v
- theories/base_logic/lib/own.v 2 additions, 2 deletionstheories/base_logic/lib/own.v
- theories/base_logic/upred.v 30 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 3 additions, 3 deletionstheories/bi/lib/atomic.v
- theories/bi/monpred.v 23 additions, 16 deletionstheories/bi/monpred.v
- theories/program_logic/total_weakestpre.v 8 additions, 6 deletionstheories/program_logic/total_weakestpre.v
- theories/program_logic/weakestpre.v 8 additions, 5 deletionstheories/program_logic/weakestpre.v
- theories/proofmode/environments.v 2 additions, 0 deletionstheories/proofmode/environments.v
Loading
Please register or sign in to comment