fix

theories/simulang/na_inv/examples/data_races.v

@@ -152,7 +152,7 @@ Section data_race.
       rewrite bool_decide_eq_true_2; last done.
       sim_pures. iApply sim_expr_base. iLeft. iApply lift_post_val.
 
-      sim_pures. source_load. target_load. to_sim. sim_pures.
+      sim_pures. source_load. target_load. sim_pures.
       (* cleanup *)
       source_free. source_free. target_free. target_free. sim_pures.
       iApply (sim_bij_release (NaRead q) with "Hbij Hc Hl_t Hl_s [//]").

theories/simulang/tactics.v

@@ -384,10 +384,14 @@ Ltac simpl_subst :=
       let e' := W.of_expr e in
       simple refine (W.tac_to_expr_subst _ _ _ _ e' _ _ _ _); [ shelve
       | simpl; rewrite ?list_to_map_to_list; reflexivity
-      | simpl; compute_done
+      | 
+          (* FIXME: really hacky hack to speed up goals on which [compute_done] takes forever due to evars, 
+              but where [simpl] would suffice...*)
+          first [timeout 1 compute_done | simpl; reflexivity]
       |];
       simple refine (W.tac_to_expr_combine_subst_map _ _ _ _ _); [ shelve |
-      simpl; compute_done | ];
+      (* FIXME *)
+      first [timeout 1 compute_done | simpl; reflexivity] | ];
       simpl
     end.
 Arguments subst : simpl never.