diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
index 3b7db3c4a..0ef1c9067 100644
--- a/src/ecLowGoal.ml
+++ b/src/ecLowGoal.ml
@@ -423,13 +423,11 @@ let rec t_lazy_match ?(reduce = `Full) ?(texn = fun _ -> raise InvalidGoalShape)
       | `None    -> raise InvalidGoalShape
       | `Full    -> EcReduction.full_red
       | `NoDelta -> EcReduction.nodelta in
-    (* honor proof-local [-delta op] opacity overrides without changing
-       which simplify databases the strategy consults *)
+    (* the proof-local simplify context (activated databases, local
+       rules, opacity overrides) applies to these head reductions too *)
     let strategy =
       { strategy with
-          EcReduction.user_local =
-            EcEnv.SimplifyContext.opacity_only
-              (FApi.tc1_simplify_context tc) } in
+          EcReduction.user_local = FApi.tc1_simplify_context tc } in
     FApi.t_seq (FApi.t_or (t_hred_with_info strategy) texn) (t_lazy_match ~reduce tx) tc
 
 (* -------------------------------------------------------------------- *)
@@ -2549,11 +2547,11 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =
     { cs_undosubst = Sid.empty (*Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) ;
       cs_sbeq = (* Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) Sid.empty;
     } in
+  (* the closing pass sees the proof-local simplify context (activated
+     databases, local rules, opacity overrides), as the entry pass does *)
   let final =
     { EcReduction.nodelta with
-        EcReduction.user_local =
-          EcEnv.SimplifyContext.opacity_only
-            (FApi.tc1_simplify_context tc) } in
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in
   FApi.t_seq (entry state) (t_simplify_with_info final) tc
 
 
@@ -2926,11 +2924,11 @@ let t_crush_fwd ?(delta = true) nb_intros (tc : tcenv1) =
     | _ -> t_fail tc
   in
 
+  (* the closing pass sees the proof-local simplify context (activated
+     databases, local rules, opacity overrides), as the entry pass does *)
   let final =
     { EcReduction.nodelta with
-        EcReduction.user_local =
-          EcEnv.SimplifyContext.opacity_only
-            (FApi.tc1_simplify_context tc) } in
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in
   FApi.t_seq
     (aux0 nb_intros)
     (t_simplify_with_info final) tc
diff --git a/tests/hint-db-crush.ec b/tests/hint-db-crush.ec
new file mode 100644
index 000000000..05b3458f8
--- /dev/null
+++ b/tests/hint-db-crush.ec
@@ -0,0 +1,17 @@
+(* A rule of an activated database applies inside crush even when the
+   term it rewrites only appears after a delta step: the head reductions
+   of split/elim see the activated databases too. *)
+require import AllCore.
+
+op c : int.
+op g : int -> bool.
+op sw (x y : int) = (y, x).
+
+axiom gE : g c = true.
+hint simplify in db : gE.
+
+lemma crush_db : g (sw c c).`2.
+proof. hint +db. by move=> />. qed.
+
+lemma crush_db_split (b : bool) : b => g (sw c c).`2 /\ b.
+proof. hint +db. by move=> />. qed.