diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 78e1f98a2f0ee1a1dcf80500db406dcf09177723..5c3e7df8a0f5b001352aa8644f46daf32fd29d35 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,6 +11,7 @@ buildjob:
   - make validate
   only:
   - master
+  - timing
   artifacts:
     paths:
     - build-time.txt
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 5f1836dc3320e4f90b3046d773aed78ca1a0a002..e36059cc4c08c9d1d85757312c78cc8ae49f6e5d 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -217,8 +217,8 @@ Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
   F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
 Proof.
   iIntros (??) "HP".
-  iMod (fupd_intro_mask') as "HM1"; first fast_done. iMod "HP".
-  iMod (fupd_intro_mask') as "HM2"; first fast_done. iModIntro.
+  iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
+  iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
   iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
 Qed.
 
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 6c9bb2693b48773c2524b92308f9d7e24017eca5..de4e0560922a072bc4db49bb8f51697f57237bf5 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -40,7 +40,11 @@ Tactic Notation "intuition" := intuition auto.
    we have x = y in the context, we will typically want to use the
    assumption and not reflexivity *)
 Ltac fast_done :=
-  solve [ eassumption | symmetry; eassumption | reflexivity ].
+  solve
+    [ eassumption
+    | symmetry; eassumption
+    | apply not_symmetry; eassumption
+    | reflexivity ].
 Tactic Notation "fast_by" tactic(tac) :=
   tac; fast_done.
 
@@ -50,16 +54,21 @@ to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
 unfolding setoid equalities. Note that this tactic performs much better than
 Coq's [easy] tactic as it does not perform [inversion]. *)
 Ltac done :=
-  trivial; intros; solve
+  solve
   [ repeat first
     [ fast_done
     | solve [trivial]
+    (* All the tactics below will introduce themselves anyway, or make no sense
+       for goals of product type. So this is a good place for us to do it. *)
+    | progress intros
     | solve [symmetry; trivial]
+    | solve [apply not_symmetry; trivial]
     | discriminate
     | contradiction
-    | solve [apply not_symmetry; trivial]
-    | split ]
-  | match goal with H : ¬_ |- _ => solve [case H; trivial] end ].
+    | split
+    | match goal with H : ¬_ |- _ => case H; clear H; done end
+    ]
+  ].
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
@@ -477,12 +486,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
   (**i simplify and solve equalities *)
   | |- _ => progress simplify_eq/=
   (**i solve the goal *)
-  | |- _ =>
-    solve
-    [ eassumption
-    | symmetry; eassumption
-    | apply not_symmetry; eassumption
-    | reflexivity ]
+  | |- _ => fast_done
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
   | |- Is_true (bool_decide _) => apply (bool_decide_pack _)