iCombineOwn now takes as and gives arguments, makes behaviour more predictable for the user.
Showing
- _CoqProject 3 additions, 3 deletions_CoqProject
- iris/base_logic/lib/cancelable_invariants.v 1 addition, 1 deletioniris/base_logic/lib/cancelable_invariants.v
- iris/base_logic/lib/gen_heap.v 2 additions, 2 deletionsiris/base_logic/lib/gen_heap.v
- iris/base_logic/lib/gen_inv_heap.v 2 additions, 6 deletionsiris/base_logic/lib/gen_inv_heap.v
- iris/base_logic/lib/ghost_map.v 3 additions, 4 deletionsiris/base_logic/lib/ghost_map.v
- iris/base_logic/lib/ghost_var.v 1 addition, 2 deletionsiris/base_logic/lib/ghost_var.v
- iris/base_logic/lib/mono_nat.v 3 additions, 3 deletionsiris/base_logic/lib/mono_nat.v
- iris/base_logic/lib/na_invariants.v 2 additions, 2 deletionsiris/base_logic/lib/na_invariants.v
- iris/base_logic/lib/proofmode_classes.v 66 additions, 0 deletionsiris/base_logic/lib/proofmode_classes.v
- iris/base_logic/lib/proofmode_instances.v 164 additions, 24 deletionsiris/base_logic/lib/proofmode_instances.v
- iris/base_logic/lib/saved_prop.v 1 addition, 1 deletioniris/base_logic/lib/saved_prop.v
- iris/base_logic/lib/validity_tactics.v 155 additions, 0 deletionsiris/base_logic/lib/validity_tactics.v
- iris/base_logic/lib/wsat.v 2 additions, 2 deletionsiris/base_logic/lib/wsat.v
- iris/base_logic/proofmode_classes.v 0 additions, 105 deletionsiris/base_logic/proofmode_classes.v
- iris/program_logic/ownp.v 3 additions, 3 deletionsiris/program_logic/ownp.v
- iris_heap_lang/lib/counter.v 4 additions, 4 deletionsiris_heap_lang/lib/counter.v
- iris_heap_lang/lib/spawn.v 1 addition, 1 deletioniris_heap_lang/lib/spawn.v
- iris_heap_lang/lib/spin_lock.v 1 addition, 1 deletioniris_heap_lang/lib/spin_lock.v
- iris_heap_lang/lib/ticket_lock.v 5 additions, 5 deletionsiris_heap_lang/lib/ticket_lock.v
Loading
Please register or sign in to comment