Unify plain and persistent modality.
This way, we do not have to duplicate a lot of theory, and we made sure that we have all lemmas/class instances for both modalities.
Showing
- theories/base_logic/big_op.v 19 additions, 19 deletionstheories/base_logic/big_op.v
- theories/base_logic/derived.v 151 additions, 296 deletionstheories/base_logic/derived.v
- theories/base_logic/lib/auth.v 3 additions, 2 deletionstheories/base_logic/lib/auth.v
- theories/base_logic/lib/boxes.v 1 addition, 1 deletiontheories/base_logic/lib/boxes.v
- theories/base_logic/lib/cancelable_invariants.v 1 addition, 1 deletiontheories/base_logic/lib/cancelable_invariants.v
- theories/base_logic/lib/core.v 6 additions, 6 deletionstheories/base_logic/lib/core.v
- theories/base_logic/lib/counter_examples.v 4 additions, 4 deletionstheories/base_logic/lib/counter_examples.v
- theories/base_logic/lib/fancy_updates.v 6 additions, 6 deletionstheories/base_logic/lib/fancy_updates.v
- theories/base_logic/lib/fancy_updates_from_vs.v 2 additions, 2 deletionstheories/base_logic/lib/fancy_updates_from_vs.v
- theories/base_logic/lib/fractional.v 1 addition, 1 deletiontheories/base_logic/lib/fractional.v
- theories/base_logic/lib/invariants.v 1 addition, 1 deletiontheories/base_logic/lib/invariants.v
- theories/base_logic/lib/na_invariants.v 1 addition, 1 deletiontheories/base_logic/lib/na_invariants.v
- theories/base_logic/lib/own.v 1 addition, 1 deletiontheories/base_logic/lib/own.v
- theories/base_logic/lib/saved_prop.v 2 additions, 1 deletiontheories/base_logic/lib/saved_prop.v
- theories/base_logic/lib/sts.v 3 additions, 3 deletionstheories/base_logic/lib/sts.v
- theories/base_logic/lib/wsat.v 1 addition, 1 deletiontheories/base_logic/lib/wsat.v
- theories/base_logic/primitive.v 44 additions, 68 deletionstheories/base_logic/primitive.v
- theories/heap_lang/lib/counter.v 1 addition, 1 deletiontheories/heap_lang/lib/counter.v
- theories/heap_lang/lib/lock.v 1 addition, 1 deletiontheories/heap_lang/lib/lock.v
- theories/heap_lang/lib/spin_lock.v 1 addition, 1 deletiontheories/heap_lang/lib/spin_lock.v
Loading
Please register or sign in to comment