Merge branch 'ike/frame_exist' into 'master'
Fix broken proofs for improved iFrame ∃ See merge request iris/examples!65
Showing
- coq-iris-examples.opam 1 addition, 1 deletioncoq-iris-examples.opam
- theories/concurrent_stacks/concurrent_stack3.v 1 addition, 1 deletiontheories/concurrent_stacks/concurrent_stack3.v
- theories/concurrent_stacks/concurrent_stack4.v 1 addition, 1 deletiontheories/concurrent_stacks/concurrent_stack4.v
- theories/hocap/concurrent_runners.v 4 additions, 5 deletionstheories/hocap/concurrent_runners.v
- theories/lecture_notes/lists.v 4 additions, 5 deletionstheories/lecture_notes/lists.v
- theories/lecture_notes/stack.v 2 additions, 4 deletionstheories/lecture_notes/stack.v
- theories/locks/array_based_queuing_lock/abql.v 1 addition, 2 deletionstheories/locks/array_based_queuing_lock/abql.v
- theories/locks/freeable_lock/freeable_logatom_lock.v 1 addition, 2 deletionstheories/locks/freeable_lock/freeable_logatom_lock.v
- theories/logatom/conditional_increment/cinc.v 3 additions, 4 deletionstheories/logatom/conditional_increment/cinc.v
- theories/logatom/counter_with_backup/counter_proof.v 8 additions, 11 deletionstheories/logatom/counter_with_backup/counter_proof.v
- theories/logatom/flat_combiner/flat.v 7 additions, 12 deletionstheories/logatom/flat_combiner/flat.v
- theories/logatom/flat_combiner/peritem.v 4 additions, 7 deletionstheories/logatom/flat_combiner/peritem.v
- theories/logatom/herlihy_wing_queue/hwq.v 4 additions, 7 deletionstheories/logatom/herlihy_wing_queue/hwq.v
- theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v 2 additions, 3 deletions...s/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
- theories/spanning_tree/spanning.v 20 additions, 26 deletionstheories/spanning_tree/spanning.v
Loading
Please register or sign in to comment