diff --git a/doc/tactics/hint-simplify.rst b/doc/tactics/hint-simplify.rst
new file mode 100644
index 000000000..adbad99ce
--- /dev/null
+++ b/doc/tactics/hint-simplify.rst
@@ -0,0 +1,228 @@
+========================================================================
+Hints: `hint simplify`
+========================================================================
+
+The `hint simplify` commands manage user reduction rules used by
+`simplify`, `cbv`, and tactics that rely on the same simplification
+machinery.
+
+Hints can be declared globally in a theory, selected through named
+databases, and adjusted locally inside a proof.
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Global declarations
+------------------------------------------------------------------------
+
+Global declarations add lemmas to a simplification database.
+
+.. admonition:: Syntax
+
+   `hint simplify {lemma}+ .`
+
+Add the listed lemmas to the default simplification database.
+
+.. admonition:: Syntax
+
+   `hint simplify in {db} : {lemma}+ .`
+
+Add the listed lemmas to the named database `{db}`.
+
+These commands are theory-level declarations: once imported, the
+corresponding rules are available to simplification.
+
+------------------------------------------------------------------------
+Using named databases
+------------------------------------------------------------------------
+
+The `simplify` and `cbv` tactics can select a named database explicitly.
+
+.. admonition:: Syntax
+
+   `simplify hint {db}`
+
+.. admonition:: Syntax
+
+   `cbv hint {db}`
+
+Without `hint {db}`, simplification uses the default database unless a
+proof-local default has been configured.
+
+------------------------------------------------------------------------
+Filtering by head symbol
+------------------------------------------------------------------------
+
+User reduction can be restricted to rules whose left-hand side is headed
+by selected symbols.
+
+.. admonition:: Syntax
+
+   `simplify with {symbol}+`
+
+Only use user reduction rules headed by one of the listed symbols.
+
+.. admonition:: Syntax
+
+   `simplify with - {symbol}+`
+
+Use user reduction rules except those headed by one of the listed
+symbols.
+
+The same forms are accepted by `cbv`. Head filters combine with named
+databases, for example `simplify with f g hint ring`.
+
+------------------------------------------------------------------------
+Proof-local modifications
+------------------------------------------------------------------------
+
+Inside a proof, the active simplify configuration can be changed without
+modifying the theory-level declarations.
+
+.. admonition:: Syntax
+
+   `hint +db simplify {db}+ .`
+
+Activate the named databases locally for the current proof state.
+
+.. admonition:: Syntax
+
+   `hint -db simplify {db}+ .`
+
+Deactivate the named databases locally for the current proof state.
+
+.. admonition:: Syntax
+
+   `hint +simplify {lemma}+ .`
+
+.. admonition:: Syntax
+
+   `hint +simplify in {db} {lemma}+ .`
+
+Add the listed lemmas locally to the default database or to the named
+database `{db}`.
+
+.. admonition:: Syntax
+
+   `hint -simplify {lemma}+ .`
+
+.. admonition:: Syntax
+
+   `hint -simplify in {db} {lemma}+ .`
+
+Remove the listed lemmas locally from the default database or from the
+named database `{db}`.
+
+.. admonition:: Syntax
+
+   `hint clear simplify .`
+
+.. admonition:: Syntax
+
+   `hint clear simplify in {db} .`
+
+Clear the local lemma additions and removals for the default database or
+for the named database `{db}`.
+
+These proof-local changes are part of the proof state and therefore
+follow the usual subgoal branching behavior.
+
+------------------------------------------------------------------------
+Proof-local defaults
+------------------------------------------------------------------------
+
+Inside a proof, defaults for future calls to `simplify` and `cbv` can be
+configured.
+
+.. admonition:: Syntax
+
+   `hint simplify hint {db} .`
+
+Set the default simplification database used by later `simplify` and
+`cbv` calls that do not explicitly choose a database.
+
+.. admonition:: Syntax
+
+   `hint simplify with {symbol}+ .`
+
+.. admonition:: Syntax
+
+   `hint simplify with - {symbol}+ .`
+
+Set the default head filter used by later `simplify` and `cbv` calls
+that do not explicitly choose one.
+
+.. admonition:: Syntax
+
+   `hint simplify clear .`
+
+Clear the proof-local defaults.
+
+Explicit arguments on `simplify` and `cbv` always take precedence over
+these proof-local defaults.
+
+------------------------------------------------------------------------
+Scoped application
+------------------------------------------------------------------------
+
+Any proof-local hint command can be used as a scoped wrapper around a
+tactic.
+
+.. admonition:: Syntax
+
+   `with hint {command} ( {tactic} )`
+
+For example:
+
+.. code-block:: easycrypt
+
+   with hint +db simplify ring (simplify).
+   with hint +simplify fooE (rewrite foo /=).
+   with hint simplify hint ring (cbv).
+
+The wrapped tactic runs with the modified hint configuration, but the
+subgoals produced afterwards are restored to the original configuration.
+
+------------------------------------------------------------------------
+Example
+------------------------------------------------------------------------
+
+.. ecproof::
+   :title: Simplify hint databases
+
+   require import AllCore Int.
+
+   op wrap1 (x : int) = x + 1.
+   op wrap2 (x : int) = x + 2.
+   op box   (x : int) = x.
+
+   lemma wrap1E x : box (wrap1 x) = box (x + 1).
+   proof. smt(). qed.
+
+   lemma wrap2E x : box (wrap2 x) = box (x + 2).
+   proof. smt(). qed.
+
+   hint simplify wrap1E.
+   hint simplify in named : wrap2E.
+
+   lemma demo_default (x : int) :
+     box (wrap1 x) = box (x + 1).
+   proof.
+     simplify.
+     trivial.
+   qed.
+
+   lemma demo_named (x : int) :
+     box (wrap2 x) = box (x + 2).
+   proof.
+     simplify hint named.
+     trivial.
+   qed.
+
+   lemma demo_local_default (x : int) :
+     box (wrap2 x) = box (x + 2).
+   proof.
+     with hint simplify hint named (simplify).
+     trivial.
+   qed.
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index e90518ff0..bc2e6065b 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -315,18 +315,11 @@ module HiPrinting = struct
   let pr_hint_simplify (fmt : Format.formatter) (env : EcEnv.env) =
     let open EcTheory in
 
-    let (hint_simplify: (EcEnv.Reduction.topsym * rule list) list) = EcEnv.Reduction.all env in
-
-    let hint_simplify = List.filter_map (fun (ts, rl) ->
-      match ts with
-      | `Path p -> Some (p, rl)
-      | _ -> None
-    ) hint_simplify
-    in
+    let hint_simplify = EcEnv.Reduction.all env in
 
     let ppe = EcPrinting.PPEnv.ofenv env in
 
-    let pp_hint_simplify ppe fmt = (fun (p,  (rls : rule list)) ->
+    let pp_rules ppe fmt = (fun (p,  (rls : rule list)) ->
       Format.fprintf fmt "@[<b 2>%s:@\n%a@]" (EcPath.basename p)
         (EcPrinting.pp_list "@\n" (fun fmt rl ->
           begin match rl.rl_cond with
@@ -341,7 +334,21 @@ module HiPrinting = struct
       )
     in
 
-    EcPrinting.pp_by_theory ppe pp_hint_simplify fmt hint_simplify
+    let pp_db fmt (base, entries) =
+      let entries = List.filter_map (fun (ts, rl) ->
+        match ts with
+        | `Path p -> Some (p, rl)
+        | _ -> None
+      ) entries in
+
+      if not (List.is_empty entries) then
+        Format.fprintf fmt "@[<v 2>%s:@\n%a@]"
+          (if base = EcEnv.Reduction.dname then "<default>" else base)
+          (EcPrinting.pp_by_theory ppe pp_rules) entries
+    in
+
+    EcPrinting.pp_list "@.@." pp_db fmt
+      (List.filter (fun (_, entries) -> not (List.is_empty entries)) hint_simplify)
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml
index 4b75e5b0c..d2c4c9db8 100644
--- a/src/ecCoreGoal.ml
+++ b/src/ecCoreGoal.ml
@@ -141,6 +141,7 @@ and pregoal = {
   g_uid   : handle;                     (* this goal ID *)
   g_hyps  : LDecl.hyps;                 (* goal local environment *)
   g_concl : form;                       (* goal conclusion *)
+  g_simpl : EcEnv.local_simplify;       (* proof-local simplify context *)
 }
 
 and goal = {
@@ -393,7 +394,7 @@ module FApi = struct
 
   (* ------------------------------------------------------------------ *)
   let tc1_flat ?target (tc : tcenv1) =
-    let { g_hyps; g_concl } = tc1_current tc in
+    let { g_hyps; g_concl; _ } = tc1_current tc in
     match target with
     | None   -> (g_hyps, g_concl)
     | Some h -> (LDecl.local_hyps h g_hyps, LDecl.hyp_by_id h g_hyps)
@@ -410,6 +411,7 @@ module FApi = struct
   let tc1_penv (tc : tcenv1) = tc.tce_penv
   let tc1_goal (tc : tcenv1) = snd (tc1_flat tc)
   let tc1_env  (tc : tcenv1) = LDecl.toenv (tc1_hyps tc)
+  let tc1_local_simplify (tc : tcenv1) = (tc1_current tc).g_simpl
 
   (* ------------------------------------------------------------------ *)
   let tc_handle (tc : tcenv) = tc1_handle tc.tce_tcenv
@@ -460,7 +462,7 @@ module FApi = struct
   (* ------------------------------------------------------------------ *)
   let pf_newgoal (pe : proofenv) ?vx hyps concl =
     let hid     = ID.gen () in
-    let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; } in
+    let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; g_simpl = EcEnv.LocalSimplify.empty; } in
     let goal    = { g_goal = pregoal; g_validation = vx; } in
     let pe      = { pe with pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals; } in
       (pe, pregoal)
@@ -469,6 +471,8 @@ module FApi = struct
   let newgoal (tc : tcenv) ?(hyps : LDecl.hyps option) (concl : form) =
     let hyps     = ofdfl (fun () -> tc_hyps tc) hyps in
     let (pe, pg) = pf_newgoal (tc_penv tc) hyps concl in
+    let pg = { pg with g_simpl = tc1_local_simplify tc.tce_tcenv } in
+    let pe = update_goal_map (fun g -> { g with g_goal = pg }) pg.g_uid pe in
 
     let tc = tc_update_tcenv (fun te -> { te with tce_penv = pe }) tc in
     let tc = { tc with tce_goals = tc.tce_goals @ [pg.g_uid] } in
@@ -506,6 +510,14 @@ module FApi = struct
     let tc = mutate (tcenv_of_tcenv1 tc) vx ?hyps fp in
     assert (tc.tce_goals = []); tc.tce_tcenv
 
+  let map_pregoal1 (tx : pregoal -> pregoal) (tc : tcenv1) =
+    let current = tc1_current tc in
+    let current = tx current in
+    let tc =
+      tc1_update_goal_map (fun g -> { g with g_goal = current }) current.g_uid tc
+    in
+    { tc with tce_goal = Some current }
+
   (* ------------------------------------------------------------------ *)
   let xmutate (tc : tcenv) (vx : 'a) (fp : form list) =
     let (tc, hds) = List.map_fold (fun tc fp -> newgoal tc fp) tc fp in
@@ -989,7 +1001,7 @@ let start (hyps : LDecl.hyps) (goal : form) =
   let uid = ID.gen () in
   let hid = ID.gen () in
 
-  let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; } in
+  let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; g_simpl = EcEnv.LocalSimplify.empty; } in
   let goal = { g_goal = goal; g_validation = None; } in
   let env  = { pr_uid   = uid;
                pr_main  = hid;
diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli
index f574b49bf..243e63413 100644
--- a/src/ecCoreGoal.mli
+++ b/src/ecCoreGoal.mli
@@ -144,6 +144,7 @@ type pregoal = {
   g_uid   : handle;
   g_hyps  : LDecl.hyps;
   g_concl : form;
+  g_simpl : EcEnv.local_simplify;
 }
 
 type validation =
@@ -279,6 +280,7 @@ module FApi : sig
    * focused goal local context. *)
   val mutate  : tcenv  -> (handle -> validation) -> ?hyps:LDecl.hyps -> form -> tcenv
   val mutate1 : tcenv1 -> (handle -> validation) -> ?hyps:LDecl.hyps -> form -> tcenv1
+  val map_pregoal1 : (pregoal -> pregoal) -> tcenv1 -> tcenv1
 
   (* Same as xmutate, but for an external node resolution depending on
    * a unbounded numbers of premises. The ['a] argument is the external
@@ -321,6 +323,7 @@ module FApi : sig
   val tc1_hyps   : ?target:ident -> tcenv1 -> LDecl.hyps
   val tc1_goal   : tcenv1 -> form
   val tc1_env    : tcenv1 -> EcEnv.env
+  val tc1_local_simplify : tcenv1 -> EcEnv.local_simplify
 
   (* Low-level tactic markers *)
   val t_low0 : string -> backward -> backward
diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index 8a449a779..e32c4eff9 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -187,7 +187,7 @@ type preenv = {
   env_tc       : TC.graph;
   env_rwbase   : Sp.t Mip.t;
   env_atbase   : atbase Msym.t;
-  env_redbase  : mredinfo;
+  env_redbase  : mredinfo Msym.t;
   env_ntbase   : ntbase Mop.t;
   env_albase   : path Mp.t;             (* theory aliases   *)
   env_modlcs   : Sid.t;                 (* declared modules *)
@@ -217,9 +217,11 @@ and tcinstance = [
   | `General of EcPath.path
 ]
 
+and redentry = EcPath.path * EcTheory.rule
+
 and redinfo =
-  { ri_priomap : (EcTheory.rule list) Mint.t;
-    ri_list    : (EcTheory.rule list) Lazy.t; }
+  { ri_priomap : (redentry list) Mint.t;
+    ri_list    : (redentry list) Lazy.t; }
 
 and mredinfo = redinfo Mrd.t
 
@@ -316,7 +318,7 @@ let empty gstate =
     env_tc       = TC.Graph.empty;
     env_rwbase   = Mip.empty;
     env_atbase   = Msym.empty;
-    env_redbase  = Mrd.empty;
+    env_redbase  = Msym.empty;
     env_ntbase   = Mop.empty;
     env_albase   = Mp.empty;
     env_modlcs   = Sid.empty;
@@ -1487,10 +1489,14 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Reduction = struct
+  type entry  = redentry
   type rule   = EcTheory.rule
   type topsym = red_topsym
+  type base = symbol
+
+  let dname : symbol = ""
 
-  let add_rule ((_, rule) : path * rule option) (db : mredinfo) =
+  let add_rule ((src, rule) : path * rule option) (db : mredinfo) =
     match rule with None -> db | Some rule ->
 
     let p : topsym =
@@ -1507,7 +1513,7 @@ module Reduction = struct
         | Some x -> x in
 
       let ri_priomap =
-        let change prules = Some (odfl [] prules @ [rule]) in
+        let change prules = Some (odfl [] prules @ [(src, rule)]) in
         Mint.change change (abs rule.rl_prio) ri_priomap in
 
       let ri_list =
@@ -1518,26 +1524,132 @@ module Reduction = struct
   let add_rules (rules : (path * rule option) list) (db : mredinfo) =
     List.fold_left ((^~) add_rule) db rules
 
-  let add ?(import = true) (rules : (path * rule_option * rule option) list) (env : env) =
-    let rstrip = List.map (fun (x, _, y) -> (x, y)) rules in
+  let updatedb ?(base : symbol option) (rules : (path * rule option) list) (db : mredinfo Msym.t) =
+    let nbase = odfl dname base in
+    let base = Msym.find_def Mrd.empty nbase db in
+    Msym.add nbase (add_rules rules base) db
+
+  let add ?(import = true) ({ red_base; red_rules } : reduction_rule) (env : env) =
+    let rstrip = List.map (fun (x, _, y) -> (x, y)) red_rules in
 
     { env with
-        env_redbase = add_rules rstrip env.env_redbase;
-        env_item = mkitem ~import (Th_reduction rules) :: env.env_item; }
+        env_redbase = updatedb ?base:red_base rstrip env.env_redbase;
+        env_item = mkitem ~import (Th_reduction { red_base; red_rules }) :: env.env_item; }
 
-  let add1 (prule : path * rule_option * rule option) (env : env) =
-    add [prule] env
+  let add1 ?base (prule : path * rule_option * rule option) (env : env) =
+    add { red_base = base; red_rules = [prule] } env
 
-  let get (p : topsym) (env : env) =
-    Mrd.find_opt p env.env_redbase
+  let get_entries ?base (p : topsym) (env : env) =
+    Msym.find_opt (odfl dname base) env.env_redbase
+    |> obind (Mrd.find_opt p)
     |> omap (fun x -> Lazy.force x.ri_list)
     |> odfl []
 
-  (* FIXME: handle other cases, right now only used for print hint *)
+  let get ?base (p : topsym) (env : env) =
+    List.map snd (get_entries ?base p env)
+
+  let getx (base : symbol) (env : env) =
+    Msym.find_def Mrd.empty base env.env_redbase
+    |> Mrd.bindings
+    |> List.map (fun (ts, mr) -> (ts, List.map snd (Lazy.force mr.ri_list)))
+
   let all (env : env) =
-    List.map (fun (ts, mr) ->
-      (ts, Lazy.force mr.ri_list))
-    (Mrd.bindings env.env_redbase)
+    Msym.bindings env.env_redbase
+    |> List.map (fun (base, db) ->
+      (base, List.map (fun (ts, mr) -> (ts, List.map snd (Lazy.force mr.ri_list))) (Mrd.bindings db)))
+end
+
+type local_simplify = {
+  ls_active  : Ssym.t;
+  ls_default_db : symbol option option;
+  ls_default_hd : [`Include of Sp.t | `Exclude of Sp.t] option;
+  ls_added   : Reduction.entry list Msym.t;
+  ls_removed : Sp.t Msym.t;
+}
+
+module LocalSimplify = struct
+  let empty = {
+    ls_active  = Ssym.singleton Reduction.dname;
+    ls_default_db = None;
+    ls_default_hd = None;
+    ls_added   = Msym.empty;
+    ls_removed = Msym.empty;
+  }
+
+  let active ls = ls.ls_active
+  let default_db ls = ls.ls_default_db
+  let default_hd ls = ls.ls_default_hd
+
+  let normbase = function
+    | Some "default" | None -> Reduction.dname
+    | Some base -> base
+
+  let activate bases ls =
+    { ls with ls_active = List.fold_left (fun st b -> Ssym.add (normbase (Some b)) st) ls.ls_active bases }
+
+  let deactivate bases ls =
+    { ls with ls_active = List.fold_left (fun st b -> Ssym.remove (normbase (Some b)) st) ls.ls_active bases }
+
+  let set_default_db base ls =
+    { ls with ls_default_db = Some (Some (normbase (Some base))) }
+
+  let set_default_hd hd ls =
+    let hd = hd |> omap (fun (mode, paths) ->
+      let paths = List.fold_left (fun acc p -> Sp.add p acc) Sp.empty paths in
+      match mode with
+      | `Include -> `Include paths
+      | `Exclude -> `Exclude paths)
+    in
+    { ls with ls_default_hd = hd }
+
+  let clear_default ls =
+    { ls with ls_default_db = None; ls_default_hd = None }
+
+  let added ?base ls =
+    Msym.find_def [] (normbase base) ls.ls_added
+
+  let removed ?base ls =
+    Msym.find_def Sp.empty (normbase base) ls.ls_removed
+
+  let add_rules ?base rules ls =
+    let base = normbase base in
+    let old = Msym.find_def [] base ls.ls_added in
+    let old =
+      List.filter (fun (p, _) ->
+        not (List.exists (fun (p', _) -> EcPath.p_equal p p') rules))
+        old
+    in
+    let ls_added = Msym.add base (old @ rules) ls.ls_added in
+    let ls_removed =
+      let removed = Msym.find_def Sp.empty base ls.ls_removed in
+      let removed = List.fold_left (fun st (p, _) -> Sp.remove p st) removed rules in
+      Msym.add base removed ls.ls_removed
+    in
+    { ls with ls_added; ls_removed }
+
+  let remove_paths ?base paths ls =
+    let base = normbase base in
+    let ls_added =
+      let added = Msym.find_def [] base ls.ls_added in
+      let added =
+        List.filter (fun (p, _) ->
+          not (List.exists (EcPath.p_equal p) paths))
+          added
+      in
+      Msym.add base added ls.ls_added
+    in
+    let ls_removed =
+      let removed = Msym.find_def Sp.empty base ls.ls_removed in
+      let removed = List.fold_left (fun st p -> Sp.add p st) removed paths in
+      Msym.add base removed ls.ls_removed
+    in
+    { ls with ls_added; ls_removed }
+
+  let clear ?base ls =
+    let base = normbase base in
+    { ls with
+        ls_added = Msym.remove base ls.ls_added;
+        ls_removed = Msym.remove base ls.ls_removed; }
 end
 
 (* -------------------------------------------------------------------- *)
@@ -3003,9 +3115,9 @@ module Theory = struct
   (* ------------------------------------------------------------------ *)
   let bind_rd_th =
     let for1 _path db = function
-      | Th_reduction rules ->
-         let rules = List.map (fun (x, _, y) -> (x, y)) rules in
-         Some (Reduction.add_rules rules db)
+      | Th_reduction { red_base; red_rules } ->
+         let rules = List.map (fun (x, _, y) -> (x, y)) red_rules in
+         Some (Reduction.updatedb ?base:red_base rules db)
       | _ -> None
 
     in bind_base_th for1
diff --git a/src/ecEnv.mli b/src/ecEnv.mli
index 04354a391..520d85642 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -420,13 +420,38 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Reduction : sig
+  type entry = path * EcTheory.rule
   type rule   = EcTheory.rule
   type topsym = [ `Path of path | `Tuple | `Proj of int]
+  type base = symbol
+
+  val dname : symbol
+  val all : env -> (base * (topsym * rule list) list) list
+  val add1 : ?base:symbol -> path * rule_option * rule option -> env -> env
+  val add  : ?import:bool -> reduction_rule -> env -> env
+  val get  : ?base:symbol -> topsym -> env -> rule list
+  val get_entries : ?base:symbol -> topsym -> env -> entry list
+  val getx : symbol -> env -> (topsym * rule list) list
+end
 
-  val all : env -> (topsym * rule list) list
-  val add1 : path * rule_option * rule option -> env -> env
-  val add  : ?import:bool -> (path * rule_option * rule option) list -> env -> env
-  val get  : topsym -> env -> rule list
+type local_simplify
+
+module LocalSimplify : sig
+  val empty : local_simplify
+  val active : local_simplify -> Ssym.t
+  val default_db : local_simplify -> symbol option option
+  val default_hd : local_simplify -> [`Include of Sp.t | `Exclude of Sp.t] option
+  val activate : symbol list -> local_simplify -> local_simplify
+  val deactivate : symbol list -> local_simplify -> local_simplify
+  val set_default_db : symbol -> local_simplify -> local_simplify
+  val set_default_hd :
+    ([`Include | `Exclude] * path list) option -> local_simplify -> local_simplify
+  val clear_default : local_simplify -> local_simplify
+  val added : ?base:symbol -> local_simplify -> Reduction.entry list
+  val removed : ?base:symbol -> local_simplify -> Sp.t
+  val add_rules : ?base:symbol -> Reduction.entry list -> local_simplify -> local_simplify
+  val remove_paths : ?base:symbol -> path list -> local_simplify -> local_simplify
+  val clear : ?base:symbol -> local_simplify -> local_simplify
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
index c58de527f..1a6fccb96 100644
--- a/src/ecHiGoal.ml
+++ b/src/ecHiGoal.ml
@@ -90,9 +90,70 @@ let process_change fp (tc : tcenv1) =
   let fp = TTC.tc1_process_formula tc fp in
   t_change fp tc
 
+(* -------------------------------------------------------------------- *)
+let process_local_hint (hint : plocalhint) (tc : tcenv1) =
+  let env = FApi.tc1_env tc in
+  let simpl = FApi.tc1_local_simplify tc in
+
+  let process_hd ops =
+    ops |> omap (fun (mode, ops) ->
+      let ops =
+        List.fold_left (fun acc ps ->
+          match EcEnv.Op.lookup_opt (unloc ps) env with
+          | None   -> tc_lookup_error !!tc ~loc:ps.pl_loc `Operator (unloc ps)
+          | Some p -> (fst p) :: acc
+        ) [] ops
+      in
+      (mode, List.rev ops))
+  in
+
+  let simpl =
+    match hint with
+    | PLHDb (`Add, dbs) ->
+        EcEnv.LocalSimplify.activate dbs simpl
+
+    | PLHDb (`Remove, dbs) ->
+        EcEnv.LocalSimplify.deactivate dbs simpl
+
+    | PLHLemmas (mode, base, lemmas) ->
+        let opts = EcTheory.{ ur_delta = false; ur_eqtrue = false; } in
+        let entries =
+          List.map (fun lemma ->
+            let path = EcEnv.Ax.lookup_path (unloc lemma) env in
+            let rule = EcReduction.User.compile ~opts ~prio:0 env path in
+            (path, rule)
+          ) lemmas
+        in
+        begin match mode with
+        | `Add ->
+            EcEnv.LocalSimplify.add_rules ?base entries simpl
+        | `Remove ->
+            EcEnv.LocalSimplify.remove_paths ?base (List.map fst entries) simpl
+        end
+
+    | PLHClear base ->
+        EcEnv.LocalSimplify.clear ?base simpl
+
+    | PLHDefault (db, hd) ->
+        let simpl =
+          db |> Option.fold ~none:simpl ~some:(fun db ->
+            EcEnv.LocalSimplify.set_default_db db simpl)
+        in
+        let hd = process_hd hd in
+        hd |> Option.fold ~none:simpl ~some:(fun hd ->
+          EcEnv.LocalSimplify.set_default_hd (Some hd) simpl)
+
+    | PLHClearDefault ->
+        EcEnv.LocalSimplify.clear_default simpl
+  in
+
+  FApi.tcenv_of_tcenv1
+    (FApi.map_pregoal1 (fun goal -> { goal with g_simpl = simpl }) tc)
+
 (* -------------------------------------------------------------------- *)
 let process_simplify_info ri (tc : tcenv1) =
   let env, hyps, _ = FApi.tc1_eflat tc in
+  let simpl = FApi.tc1_local_simplify tc in
 
   let do1 (sop, sid) ps =
     match ps.pl_desc with
@@ -113,6 +174,22 @@ let process_simplify_info ri (tc : tcenv1) =
       |> odfl ((fun _ -> `IfTransparent), predT)
   in
 
+  let user_hd =
+    match ri.puser_hd with
+    | None -> EcEnv.LocalSimplify.default_hd simpl
+    | Some (mode, ops) ->
+        let ops =
+          List.fold_left (fun acc ps ->
+            match EcEnv.Op.lookup_opt (unloc ps) env with
+            | None   -> tc_lookup_error !!tc ~loc:ps.pl_loc `Operator (unloc ps)
+            | Some p -> Sp.add (fst p) acc
+          ) Sp.empty ops
+        in
+        Some (match mode with
+          | `Include -> `Include ops
+          | `Exclude -> `Exclude ops)
+  in
+
   {
     EcReduction.beta    = ri.pbeta;
     EcReduction.delta_p = delta_p;
@@ -123,6 +200,15 @@ let process_simplify_info ri (tc : tcenv1) =
     EcReduction.logic   = if ri.plogic then Some `Full else None;
     EcReduction.modpath = ri.pmodpath;
     EcReduction.user    = ri.puser;
+    EcReduction.user_db =
+      (match ri.puser_db with
+       | Some _ as db -> db
+       | None -> EcEnv.LocalSimplify.default_db simpl |> odfl None);
+    EcReduction.user_local = simpl;
+    EcReduction.user_hd =
+      (match user_hd with
+       | Some _ as hd -> hd
+       | None -> EcEnv.LocalSimplify.default_hd simpl);
   }
 
 (*-------------------------------------------------------------------- *)
diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli
index 78f61f3b0..ebd928691 100644
--- a/src/ecHiGoal.mli
+++ b/src/ecHiGoal.mli
@@ -96,6 +96,7 @@ val process_congr       : backward
 val process_solve       : ?bases:symbol list -> ?depth:int -> backward
 val process_trivial     : backward
 val process_change      : pformula -> backward
+val process_local_hint  : plocalhint -> backward
 val process_simplify    : preduction -> backward
 val process_cbv         : preduction -> backward
 val process_pose        : psymbol -> ptybindings -> rwocc -> pformula -> backward
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 8a6576983..d2fffcd05 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -156,6 +156,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) =
     | Pmemory m           -> process_memory m
     | Pwlog (ids, b, f)   -> process_wlog ~suff:b ids f
     | Pgenhave gh         -> process_genhave ttenv gh
+    | PlocalHint h        -> process_local_hint h
     | Prwnormal _         -> assert false
     | Pcoq (m, n, pi)     -> process_coq ~loc:(loc t) ~name:n.pl_desc ttenv m pi
   in
@@ -328,6 +329,17 @@ and process_core (ttenv : ttenv) ({ pl_loc = loc } as t : ptactic_core) (tc : tc
     | Ptry      t           -> `One (process1_try      ttenv t)
     | Por       (t1, t2)    -> `One (process1_or       ttenv t1 t2)
     | Pseq      ts          -> `One (process1_seq      ttenv ts)
+    | Pwith     (h, ts)     -> `One (fun tc ->
+                                  let simpl = tc1_local_simplify tc in
+                                  let tc = process_local_hint h tc in
+                                  let tc = process1_seq ttenv ts (as_tcenv1 tc) in
+                                  t_onall
+                                    (fun tc ->
+                                      tcenv_of_tcenv1
+                                        (map_pregoal1
+                                           (fun goal -> { goal with g_simpl = simpl })
+                                           tc))
+                                    tc)
     | Pcase     es          -> `One (process1_case     ttenv es)
     | Pprogress (o, t)      -> `One (process1_progress ttenv o t)
     | Psubgoal  tt          -> `All (process_chain     ttenv tt)
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 117ccf9a1..fccf853ab 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -88,12 +88,12 @@
       pa_kind     = k;
       pa_locality = locality; }
 
-  let mk_simplify l =
+  let mk_simplify ?db l =
     if l = [] then
       { pbeta  = true; pzeta  = true;
         piota  = true; peta   = true;
         plogic = true; pdelta = None;
-        pmodpath = true; puser = true; }
+        pmodpath = true; puser = true; puser_db = db; puser_hd = None; }
     else
       let doarg acc = function
         | `Delta l ->
@@ -108,15 +108,20 @@
         | `Logic   -> { acc with plogic   = true }
         | `ModPath -> { acc with pmodpath = true }
         | `User    -> { acc with puser    = true }
+        | `UserHd h -> { acc with puser_hd = Some h }
       in
         List.fold_left doarg
           { pbeta  = false; pzeta  = false;
             piota  = false; peta   = false;
             plogic = false; pdelta = Some [];
-            pmodpath = false; puser = false; } l
+            pmodpath = false; puser = false; puser_db = db; puser_hd = None; } l
 
   let simplify_red = [`Zeta; `Iota; `Beta; `Eta; `Logic; `ModPath; `User]
 
+  let as_hintdb_mode = function
+    | `Plus  -> `Add
+    | `Minus -> `Remove
+
   let mk_pterm explicit head args =
     { fp_mode = if explicit then `Explicit else `Implicit;
       fp_head = head;
@@ -2492,17 +2497,37 @@ simplify_arg:
 | ETA              { `Eta }
 | LOGIC            { `Logic }
 | MODPATH          { `ModPath }
+| WITH b=boption(MINUS) l=qoident+
+    { `UserHd ((if b then `Exclude else `Include), l) }
+
+%inline simplify_db:
+| HINT x=lident { unloc x }
+
+%inline pmode:
+| PLUS  { `Plus  }
+| MINUS { `Minus }
 
 simplify:
-| l=simplify_arg+     { l }
-| SIMPLIFY            { simplify_red }
-| SIMPLIFY l=qoident+ { `Delta l  :: simplify_red  }
-| SIMPLIFY DELTA      { `Delta [] :: simplify_red }
+| l=simplify_arg+ db=simplify_db?
+    { mk_simplify ?db l }
+| SIMPLIFY l=simplify_arg+ db=simplify_db?
+    { mk_simplify ?db (`User :: l) }
+| SIMPLIFY db=simplify_db?
+    { mk_simplify ?db simplify_red }
+| SIMPLIFY l=qoident+ db=simplify_db?
+    { mk_simplify ?db (`Delta l  :: simplify_red) }
+| SIMPLIFY DELTA db=simplify_db?
+    { mk_simplify ?db (`Delta [] :: simplify_red) }
 
 cbv:
-| CBV            { simplify_red }
-| CBV l=qoident+ { `Delta l  :: simplify_red  }
-| CBV DELTA      { `Delta [] :: simplify_red }
+| CBV l=simplify_arg+ db=simplify_db?
+    { mk_simplify ?db (`User :: l) }
+| CBV db=simplify_db?
+    { mk_simplify ?db simplify_red }
+| CBV l=qoident+ db=simplify_db?
+    { mk_simplify ?db (`Delta l  :: simplify_red) }
+| CBV DELTA db=simplify_db?
+    { mk_simplify ?db (`Delta [] :: simplify_red) }
 
 conseq:
 | empty                            { None, None }
@@ -2789,6 +2814,9 @@ logtactic:
 | ASSUMPTION
     { Passumption }
 
+| HINT h=localhint_cmd
+    { PlocalHint h }
+
 | MOVE vw=prefix(SLASH, pterm)* gp=prefix(COLON, revert)?
    { Pmove { pr_rev = odfl prevert0 gp; pr_view = vw; } }
 
@@ -2880,10 +2908,10 @@ logtactic:
    { Papply (`Apply (es, `Exact), None) }
 
 | l=simplify
-   { Psimplify (mk_simplify l) }
+   { Psimplify l }
 
 | l=cbv
-   { Pcbv (mk_simplify l) }
+   { Pcbv l }
 
 | CHANGE f=sform
    { Pchange f }
@@ -3424,6 +3452,32 @@ caseoption:
 | n=word? NOT      { (`All, n) }
 | n=word? QUESTION { (`Maybe, n) }
 
+localhint_cmd:
+| m=pmode x=lident SIMPLIFY dbs=lident+
+    { if unloc x <> "db" then
+        parse_error x.pl_loc (Some ("invalid hint command: " ^ (unloc x)));
+      PLHDb (as_hintdb_mode m, List.map unloc dbs) }
+
+| m=pmode SIMPLIFY db=prefix(IN, lident)? l=qident+
+    { PLHLemmas (as_hintdb_mode m, omap unloc db, l) }
+
+| CLEAR SIMPLIFY db=prefix(IN, lident)?
+    { PLHClear (omap unloc db) }
+
+| SIMPLIFY db=localhint_defaultdb hd=localhint_userhd?
+    { PLHDefault (db, hd) }
+
+| SIMPLIFY CLEAR
+    { PLHClearDefault }
+
+localhint_userhd:
+| WITH b=boption(MINUS) l=qoident+
+    { ((if b then `Exclude else `Include), l) }
+
+localhint_defaultdb:
+|               { None }
+| d=simplify_db { Some d }
+
 tactic_core_r:
 | IDTAC
    { Pidtac None }
@@ -3452,6 +3506,9 @@ tactic_core_r:
 | LPAREN s=tactics RPAREN
    { Pseq s }
 
+| WITH HINT h=localhint_cmd LPAREN s=tactics RPAREN
+   { Pwith (h, s) }
+
 | ADMIT
    { Padmit }
 
@@ -3890,8 +3947,10 @@ hint:
 (* -------------------------------------------------------------------- *)
 (* User reduction                                                       *)
 reduction:
+| HINT SIMPLIFY IN db=lident COLON opt=bracket(user_red_option*)? xs=plist1(user_red_info, COMMA)
+    { (Some (unloc db), odfl [] opt, xs) }
 | HINT SIMPLIFY opt=bracket(user_red_option*)? xs=plist1(user_red_info, COMMA)
-    { (odfl [] opt, xs) }
+    { (None, odfl [] opt, xs) }
 
 user_red_info:
 | x=qident i=prefix(AT, word)?
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 7d060227e..0cba94ac4 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -568,6 +568,8 @@ type preduction = {
   plogic   : bool;                      (* logical simplification *)
   pmodpath : bool;                      (* modpath normalization *)
   puser    : bool;                      (* user reduction *)
+  puser_db : symbol option;             (* user reduction database *)
+  puser_hd : ([`Include | `Exclude] * pqsymbol list) option;
 }
 
 (* -------------------------------------------------------------------- *)
@@ -1039,6 +1041,16 @@ type clear_info = [
 (* -------------------------------------------------------------------- *)
 type pgenhave = psymbol * intropattern option * psymbol list * pformula
 
+(* -------------------------------------------------------------------- *)
+type phintdbmode = [ `Add | `Remove ]
+
+type plocalhint =
+  | PLHDb    of phintdbmode * symbol list
+  | PLHLemmas of phintdbmode * symbol option * pqsymbol list
+  | PLHClear of symbol option
+  | PLHDefault of symbol option * ([`Include | `Exclude] * pqsymbol list) option
+  | PLHClearDefault
+
 (* -------------------------------------------------------------------- *)
 type logtactic =
   | Preflexivity
@@ -1070,6 +1082,7 @@ type logtactic =
   | Pgenhave    of pgenhave
   | Pwlog       of (psymbol list * bool * pformula)
   | Pcoq        of (EcProvers.coq_mode option * psymbol * pprover_infos)
+  | PlocalHint  of plocalhint
 
 (* -------------------------------------------------------------------- *)
 and ptactic_core_r =
@@ -1086,6 +1099,7 @@ and ptactic_core_r =
   | Pprogress   of ppgoptions * ptactic_core option
   | Psubgoal    of ptactic_chain
   | Pnstrict    of ptactic_core
+  | Pwith       of plocalhint * ptactics
   | Padmit
 
 (* -------------------------------------------------------------------- *)
@@ -1326,7 +1340,7 @@ type puseroption =
   [`Delta | `EqTrue]
 
 type puserred =
-  puseroption list * (pqsymbol list * int option) list
+  symbol option * puseroption list * (pqsymbol list * int option) list
 
 type threquire =
   psymbol option * (psymbol * psymbol option) list * [`Import|`Export] option
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index b5f4e2030..cb9f4670f 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -3834,9 +3834,12 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
         pp_locality lc
         (pp_rwname ppe) p (pp_list "@ " (pp_axname ppe)) l
 
-  | EcTheory.Th_reduction _ ->
+  | EcTheory.Th_reduction { red_base; _ } ->
       (* FIXME: section we should add the lemma in the reduction *)
-      Format.fprintf fmt "hint simplify."
+      begin match red_base with
+      | None -> Format.fprintf fmt "hint simplify."
+      | Some base -> Format.fprintf fmt "hint simplify in %s : ." base
+      end
 
   | EcTheory.Th_auto { level; base; axioms; locality; } ->
       Format.fprintf fmt "%ahint solve %d %s : %a."
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index d28cb2058..9560bd89c 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -642,6 +642,9 @@ type reduction_info = {
   logic   : rlogic_info;
   modpath : bool;
   user    : bool;
+  user_db : EcSymbols.symbol option;
+  user_local : EcEnv.local_simplify;
+  user_hd : [`Include of EcPath.Sp.t | `Exclude of EcPath.Sp.t] option;
 }
 
 and deltap      = [Op.redmode | `No]
@@ -658,6 +661,9 @@ let full_red = {
   logic   = Some `Full;
   modpath = true;
   user    = true;
+  user_db = None;
+  user_local = EcEnv.LocalSimplify.empty;
+  user_hd = None;
 }
 
 let no_red = {
@@ -670,6 +676,9 @@ let no_red = {
   logic   = None;
   modpath = false;
   user    = false;
+  user_db = None;
+  user_local = EcEnv.LocalSimplify.empty;
+  user_hd = None;
 }
 
 let beta_red     = { no_red with beta = true; }
@@ -741,8 +750,41 @@ let reduce_user_gen simplify ri env hyps f =
     | Fproj (_, i) -> `Proj i
     | _ -> raise nohead in
 
-  let rules = EcEnv.Reduction.get p env in
+  begin match ri.user_hd, p with
+  | Some (`Include hs), `Path p when not (EcPath.Sp.mem p hs) -> raise nohead
+  | Some (`Exclude hs), `Path p when EcPath.Sp.mem p hs -> raise nohead
+  | _ -> ()
+  end;
+
+  let get_rules_for_base base =
+    let removed = EcEnv.LocalSimplify.removed ~base ri.user_local in
+    let rules =
+      EcEnv.Reduction.get_entries ~base p env
+      |> List.filter (fun (src, _) -> not (EcPath.Sp.mem src removed))
+      |> List.map snd
+    in
+    let added =
+      EcEnv.LocalSimplify.added ~base ri.user_local
+      |> List.filter_map (fun ((_, rule) : EcEnv.Reduction.entry) ->
+        let p' : EcEnv.Reduction.topsym =
+          match rule.rl_ptn with
+          | Rule (`Op p, _)   -> `Path (fst p)
+          | Rule (`Tuple, _)  -> `Tuple
+          | Rule (`Proj i, _) -> `Proj i
+          | Var _ | Int _     -> assert false
+        in
+        if p' = p then Some rule else None)
+    in
+    rules @ added
+  in
+
+  let bases =
+    match ri.user_db with
+    | Some base -> [if base = "default" then EcEnv.Reduction.dname else base]
+    | None -> EcSymbols.Ssym.elements (EcEnv.LocalSimplify.active ri.user_local)
+  in
 
+  let rules = List.flatten (List.map get_rules_for_base bases) in
   if rules = [] then raise nohead;
 
   let module R = EcTheory in
diff --git a/src/ecReduction.mli b/src/ecReduction.mli
index ceb057d24..f70309673 100644
--- a/src/ecReduction.mli
+++ b/src/ecReduction.mli
@@ -70,6 +70,9 @@ type reduction_info = {
   logic   : rlogic_info;       (* perform logical simplification *)
   modpath : bool;              (* reduce module path *)
   user    : bool;              (* reduce user defined rules *)
+  user_db : EcSymbols.symbol option; (* user reduction database *)
+  user_local : EcEnv.local_simplify; (* proof-local simplify overlay *)
+  user_hd : [`Include of EcPath.Sp.t | `Exclude of EcPath.Sp.t] option;
 }
 
 and deltap      = [EcEnv.Op.redmode | `No]
diff --git a/src/ecScope.ml b/src/ecScope.ml
index c7cc2fbe6..e00587a30 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -2078,7 +2078,7 @@ end
 (* -------------------------------------------------------------------- *)
 module Reduction = struct
   (* FIXME: section -> allow "local" flag *)
-  let add_reduction scope (opts, reds) =
+  let add_reduction scope (base, opts, reds) =
     check_state `InTop "hint simplify" scope;
 
     let rules =
@@ -2099,7 +2099,10 @@ module Reduction = struct
 
     in
 
-    let item = EcTheory.mkitem ~import:true (EcTheory.Th_reduction rules) in
+    let item =
+      EcTheory.mkitem ~import:true
+        (EcTheory.Th_reduction { red_base = base; red_rules = rules })
+    in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 end
 
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index 8bae12c68..b51a582e3 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -1066,10 +1066,10 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) =
   | Th_addrw (b, ls, lc) ->
       Th_addrw (subst_path s b, List.map (subst_path s) ls, lc)
 
-  | Th_reduction rules ->
-      let rules =
-        List.map (fun (p, opts, _) -> (subst_path s p, opts, None)) rules
-      in Th_reduction rules
+  | Th_reduction ({ red_rules } as red) ->
+      let red_rules =
+        List.map (fun (p, opts, _) -> (subst_path s p, opts, None)) red_rules
+      in Th_reduction { red with red_rules }
 
   | Th_auto ({ axioms } as auto_rl) ->
       Th_auto { auto_rl with axioms =
@@ -1214,4 +1214,3 @@ let inv_rebind (inv : inv) (ms : memory list) : inv =
   | Inv_ts ts, [ml; mr] -> Inv_ts (ts_inv_rebind ts ml mr)
   | Inv_hs hs, [m] -> Inv_hs (hs_inv_rebind hs m)
   | _, _ -> assert false
-
diff --git a/src/ecTheory.ml b/src/ecTheory.ml
index c4bcbfe19..5f6e375f1 100644
--- a/src/ecTheory.ml
+++ b/src/ecTheory.ml
@@ -29,7 +29,7 @@ and theory_item_r =
   | Th_instance  of (ty_params * EcTypes.ty) * tcinstance * is_local
   | Th_baserw    of symbol * is_local
   | Th_addrw     of EcPath.path * EcPath.path list * is_local
-  | Th_reduction of (EcPath.path * rule_option * rule option) list
+  | Th_reduction of reduction_rule
   | Th_auto      of auto_rule
   | Th_alias     of (symbol * path) (* FIXME: currently, only theories *)
 
@@ -69,6 +69,11 @@ and rule_option = {
   ur_eqtrue : bool;
 }
 
+and reduction_rule = {
+  red_base : symbol option;
+  red_rules : (path * rule_option * rule option) list;
+}
+
 and auto_rule = {
   level    : int;
   base     : symbol option;
diff --git a/src/ecTheory.mli b/src/ecTheory.mli
index 20c34364b..2a59ff246 100644
--- a/src/ecTheory.mli
+++ b/src/ecTheory.mli
@@ -26,7 +26,7 @@ and theory_item_r =
   | Th_baserw    of symbol * is_local
   | Th_addrw     of EcPath.path * EcPath.path list * is_local
   (* reduction rule does not survive to section so no locality *)
-  | Th_reduction of (EcPath.path * rule_option * rule option) list
+  | Th_reduction of reduction_rule
   | Th_auto      of auto_rule
   | Th_alias     of (symbol * path)
 
@@ -66,6 +66,11 @@ and rule_option = {
   ur_eqtrue : bool;
 }
 
+and reduction_rule = {
+  red_base : symbol option;
+  red_rules : (path * rule_option * rule option) list;
+}
+
 and auto_rule = {
   level    : int;
   base     : symbol option;
diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 8982a3493..7e9e5803d 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -928,7 +928,7 @@ and replay_auto
 (* -------------------------------------------------------------------- *)
 and replay_reduction
   (ove : _ ovrenv) (subst, ops, proofs, scope)
-  (import, rules : _ * (EcPath.path * EcTheory.rule_option * EcTheory.rule option) list)
+  (import, ({ red_rules } as red) : _ * EcTheory.reduction_rule)
 =
   let for1 (p, opts, rule) =
     let exception Removed in
@@ -947,8 +947,8 @@ and replay_reduction
 
     in (p, opts, rule) in
 
-  let rules = List.map for1 rules in
-  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_reduction rules) in
+  let red_rules = List.map for1 red_rules in
+  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_reduction { red with red_rules }) in
 
   (subst, ops, proofs, scope)
 
diff --git a/tests/hint_simplify_db.ec b/tests/hint_simplify_db.ec
new file mode 100644
index 000000000..e9e316eaa
--- /dev/null
+++ b/tests/hint_simplify_db.ec
@@ -0,0 +1,25 @@
+require import Int.
+
+op wrap_default : int -> int.
+op wrap_named : int -> int.
+op box : int -> int.
+
+axiom wrap_defaultE (x : int) : wrap_default x = x + 1.
+axiom wrap_namedE (x : int) : wrap_named x = x + 2.
+
+hint simplify wrap_defaultE.
+hint simplify in named: wrap_namedE.
+
+lemma wrap_default_simplifies (x : int) :
+  box (wrap_default x) = box (x + 1).
+proof.
+  simplify.
+  trivial.
+qed.
+
+lemma wrap_named_simplifies (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  simplify hint named.
+  trivial.
+qed.
diff --git a/tests/local_hint_simplify.ec b/tests/local_hint_simplify.ec
new file mode 100644
index 000000000..111248f16
--- /dev/null
+++ b/tests/local_hint_simplify.ec
@@ -0,0 +1,117 @@
+require import Int.
+
+op wrap_default : int -> int.
+op wrap_named : int -> int.
+op wrap_local : int -> int.
+op box : int -> int.
+
+axiom wrap_defaultE (x : int) : wrap_default x = x + 1.
+axiom wrap_namedE (x : int) : wrap_named x = x + 2.
+axiom wrap_localE (x : int) : wrap_local x = x + 3.
+
+hint simplify wrap_defaultE.
+hint simplify in named: wrap_namedE.
+
+lemma explicit_named_db (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  simplify hint named.
+  trivial.
+qed.
+
+lemma activate_named_db (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  hint +db simplify named.
+  simplify.
+  trivial.
+qed.
+
+lemma deactivate_default_db (x : int) :
+  box (wrap_default x) = box (x + 1).
+proof.
+  hint -db simplify default.
+  simplify.
+  hint +db simplify default.
+  simplify.
+  trivial.
+qed.
+
+lemma add_remove_clear_local_hints (x : int) :
+  box (wrap_local x) = box (x + 3).
+proof.
+  hint +simplify wrap_localE.
+  simplify.
+  trivial.
+qed.
+
+lemma remove_local_hint (x : int) :
+  box (wrap_local x) = box (x + 3).
+proof.
+  hint +simplify wrap_localE.
+  hint -simplify wrap_localE.
+  simplify.
+  hint +simplify wrap_localE.
+  hint clear simplify.
+  simplify.
+  hint +simplify wrap_localE.
+  simplify.
+  trivial.
+qed.
+
+lemma scoped_with_hint_db (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  with hint +db simplify named (simplify).
+  trivial.
+qed.
+
+lemma scoped_with_hint_lemma (x : int) :
+  box (wrap_local x) = box (x + 3).
+proof.
+  with hint +simplify wrap_localE (simplify).
+  trivial.
+qed.
+
+lemma scoped_with_hint_restores (x : int) :
+  box (wrap_local x) = box (x + 3) /\ true.
+proof.
+  with hint +simplify wrap_localE (split).
+  hint +simplify wrap_localE.
+  simplify.
+  trivial.
+  trivial.
+qed.
+
+lemma local_default_named_db (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  hint simplify hint named.
+  simplify.
+  trivial.
+qed.
+
+lemma scoped_default_named_db (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  with hint simplify hint named (simplify).
+  trivial.
+qed.
+
+lemma local_default_head_filter (x : int) :
+  box (wrap_local x) = box (x + 3).
+proof.
+  hint +simplify wrap_localE.
+  hint simplify with wrap_local.
+  simplify.
+  trivial.
+qed.
+
+lemma clear_local_default (x : int) :
+  box (wrap_named x) = box (x + 2).
+proof.
+  hint simplify hint named.
+  hint simplify clear.
+  simplify hint named.
+  trivial.
+qed.
diff --git a/tests/simplify_head_filter.ec b/tests/simplify_head_filter.ec
new file mode 100644
index 000000000..560997e2d
--- /dev/null
+++ b/tests/simplify_head_filter.ec
@@ -0,0 +1,39 @@
+require import Int.
+
+op wrap1 : int -> int.
+op wrap2 : int -> int.
+op box : int -> int.
+
+axiom wrap1E (x : int) : wrap1 x = x + 1.
+axiom wrap2E (x : int) : wrap2 x = x + 2.
+
+hint simplify wrap1E.
+hint simplify in named: wrap2E.
+
+lemma simplify_with_include (x : int) :
+  box (wrap1 x) = box (x + 1).
+proof.
+  simplify with wrap1.
+  trivial.
+qed.
+
+lemma simplify_with_exclude (x : int) :
+  box (wrap1 x) = box (x + 1).
+proof.
+  simplify with - wrap2.
+  trivial.
+qed.
+
+lemma simplify_named_with_include (x : int) :
+  box (wrap2 x) = box (x + 2).
+proof.
+  simplify with wrap2 hint named.
+  trivial.
+qed.
+
+lemma cbv_named_with_exclude (x : int) :
+  box (wrap2 x) = box (x + 2).
+proof.
+  cbv with - wrap1 hint named.
+  trivial.
+qed.