Changed namespace to diaframe, improved local_post tactic.

_CoqProject

--Q theories iris_automation
+-Q theories diaframe
 -Q external/actris/theories actris
 -Q external/lambda-rust/theories lrust
 -Q external/reloc/theories reloc

theories/examples/comparison/arc.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import frac_token.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import frac_token.
 
 Definition mk_arc : val :=
   λ: "_", ref #1.
@@ -47,7 +47,7 @@ Section spec.
   Global Program Instance count_arc_spec γ (l : loc) :
     SPEC {{ token P γ ∗ inv N (arc_inv γ l) }} 
       count #l 
-    {{ (z : Z), RET #z; ⌜0 < z⌝%Z }}.
+    {{ (z : Z), RET #z; ⌜0 < z⌝%Z ∗ token P γ }}.
 
   Global Instance drop_arc_spec γ (l : loc) :
     SPEC {{ token P γ ∗ inv N (arc_inv γ l) }} 

theories/examples/comparison/bag_stack.v

-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 
 Definition new_stack : val := 
   λ: "_", ref NONEV.

theories/examples/comparison/barrier.v

-From iris_automation.heap_lang Require Import stepping_tacs biabd_instances_heaplang.
-From iris_automation.steps Require Import local_post.
+From diaframe.heap_lang Require Import stepping_tacs biabd_instances_heaplang.
 From iris.heap_lang Require Import proofmode.
 From iris.algebra Require Import frac_auth numbers excl.
-From iris_automation.lib Require Import ticket_cmra frac_token own_hints.
+From diaframe.lib Require Import ticket_cmra frac_token own_hints.
 
 Definition make_barrier : val := 
   λ: <>, ref #0.

theories/examples/comparison/barrier_client.v

-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 From iris.algebra Require Import frac_auth numbers csum agree.
 From iris.heap_lang Require Import proofmode.
-From iris_automation.lib Require Import frac_token int_as_nat_diff own_hints.
-From iris_automation.examples.comparison Require Import barrier.
+From diaframe.lib Require Import frac_token int_as_nat_diff own_hints.
+From diaframe.examples.comparison Require Import barrier.
 
 Definition increment : val := 
   rec: "inc" "c" := 

theories/examples/comparison/bounded_counter.v

-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 From iris.heap_lang Require Import proofmode.
 From iris.algebra Require Import frac_auth.
-From iris_automation.lib Require Import Z_cmra own_hints.
+From diaframe.lib Require Import Z_cmra own_hints.
 
 Definition make_counter : val := 
   λ: <>, ref #0.

theories/examples/comparison/cas_counter.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import own_hints.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import own_hints.
 From iris.algebra Require Import frac_auth numbers.
 
 Definition make_counter : val := 

theories/examples/comparison/cas_counter_client.v

-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 From iris.algebra Require Import frac_auth numbers.
-From iris_automation.examples.comparison Require Import cas_counter fork_join.
+From diaframe.examples.comparison Require Import cas_counter fork_join.
 
 Definition thread_incr : val :=
   λ: "c" "j",

theories/examples/comparison/cas_counter_client_closed.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.examples.comparison Require Import cas_counter cas_counter_client fork_join.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.examples.comparison Require Import cas_counter cas_counter_client fork_join.
 From iris.heap_lang Require Import adequacy.
 
 Definition clientΣ : gFunctors := #[ heapΣ; counterΣ; forkjoinΣ ].

theories/examples/comparison/clh_lock.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import own_hints.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import own_hints.
 From iris.algebra Require Import agree frac excl.
 
 Definition new_lock : val :=

theories/examples/comparison/demo/cas_counter_demo.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import own_hints.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import own_hints.
 From iris.algebra Require Import frac_auth numbers.
 From iris.heap_lang Require Import proofmode.
 

theories/examples/comparison/demo/spin_lock_demo.v

 From iris.algebra Require Import excl.
-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import own_hints.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import own_hints.
 From iris.heap_lang Require Import proofmode.
 
 Definition newlock : val := 

theories/examples/comparison/demo/ticket_lock_demo.v

 From iris.algebra Require Import coPset excl auth.
-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 From iris.heap_lang Require Import proofmode.
-From iris_automation.lib Require Import ticket_cmra own_hints.
+From diaframe.lib Require Import ticket_cmra own_hints.
 
 Definition wait_loop : val :=
   rec: "wait_loop" "x" "lk" :=

theories/examples/comparison/failing/arc_failing.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import frac_token.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import frac_token.
 
 Definition mk_arc : val :=
   λ: "_", ref #1.

theories/examples/comparison/failing/bag_stack_failing.v

-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 
 Definition new_stack : val := 
   λ: "_", ref NONEV.

theories/examples/comparison/failing/cas_counter_failing.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import own_hints.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import own_hints.
 From iris.algebra Require Import frac_auth numbers.
 
 Definition make_counter : val := 

theories/examples/comparison/failing/ticket_lock_client_failing.v

-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 From iris.heap_lang.lib Require Import par.
-From iris_automation.examples.comparison Require Import ticket_lock.
+From diaframe.examples.comparison Require Import ticket_lock.
 
 Definition foo : val :=
   λ: "lk" "l" "z",

theories/examples/comparison/failing/ticket_lock_failing.v

 From iris.algebra Require Import coPset excl auth.
-From iris_automation.heap_lang Require Import stepping_tacs.
+From diaframe.heap_lang Require Import stepping_tacs.
 From iris.heap_lang Require Import proofmode.
-From iris_automation.lib Require Import ticket_cmra own_hints.
+From diaframe.lib Require Import ticket_cmra own_hints.
 
 Definition wait_loop : val :=
   rec: "wait_loop" "x" "lk" :=

theories/examples/comparison/fork_join.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.lib Require Import own_hints.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.lib Require Import own_hints.
 From iris.algebra Require Import excl.
 
 Definition make_join : val :=

theories/examples/comparison/fork_join_client.v

-From iris_automation.heap_lang Require Import stepping_tacs.
-From iris_automation.examples.comparison Require Import fork_join.
+From diaframe.heap_lang Require Import stepping_tacs.
+From diaframe.examples.comparison Require Import fork_join.
 
 Definition client_thread : val :=
   λ: "l" "c",