From 1ba0beddef2b2adc542a8d6d21b931ba0b2ac95b Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Wed, 25 Mar 2026 19:38:41 +0100
Subject: [PATCH] Add named and local simplify hint databases
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Introduce named simplify databases, a head-symbol filter, and proof-local
control over which user-reduction rules `simplify`/`cbv` apply. These are
all expressed through one `hint` clause, used in three places: after a
`simplify`/`cbv` tactic, as a standalone `hint` command, and in the
`with hint … (…)` scoped wrapper.

Theory-level declarations register lemmas into a database (unchanged):

    hint simplify {lemma}+ .             (* default database *)
    hint simplify in {db} : {lemma}+ .   (* named database   *)

On the `simplify`/`cbv` tactics, a `hint` clause chooses the rules for
that call. The clause is `hint` followed by items disambiguated by their
delimiter -- a bare name is a database, `[…]` holds operators, `{…}` holds
lemmas:

    simplify hint d1 d2                  (* consult exactly d1, d2     *)
    simplify hint +d1 -d2                (* +/- a db on the active set *)
    simplify hint +[f g]                 (* restrict user rules to f,g *)
    simplify hint {L}                    (* add lemma L for this call  *)
    cbv hint d1 {M}

The database part is either an unsigned selection (replace) or signed +/-
deltas (on the active set), never both; at most one head filter is
allowed; and lemma sets `{…}` are add-only -- a clause never removes
lemmas from a database (use the head filter to restrict which rules
apply).

The same clause, written as a standalone command, changes the proof state
persistently:

    hint +d1 -d2 .                       (* activate / deactivate DBs  *)
    hint {L} .                           (* add local lemmas           *)
    hint d1 d2 .                         (* set default databases      *)
    hint +[f g] .                        (* set default head filter    *)
    hint clear [ {db} ] .                (* clear local additions      *)
    hint clear default .                 (* clear proof-local defaults *)

and as a scoped wrapper, in effect only for the wrapped tactic and
restored on the resulting subgoals:

    with hint {clause} ( {tactic} ) .

Implementation: the proof-local simplify context lives in a new
EcSimplifyContext module (extracted from EcEnv); it is threaded through
proof goals so the active DB set, added lemmas, default database, and
head filter propagate across subgoals and are consulted by `simplify` and
`cbv`. Reduction storage and simplify-hint printing support named
databases and head filtering.

Document the syntax in doc/tactics/hint-simplify.rst and add regression
tests (tests/hint_simplify_db.ec, tests/local_hint_simplify.ec,
tests/simplify_head_filter.ec).
---
 doc/tactics/hint-simplify.rst | 188 ++++++++++++++++++++++++++++++++++
 src/ecCommands.ml             |  27 +++--
 src/ecCoreGoal.ml             |  18 +++-
 src/ecCoreGoal.mli            |   3 +
 src/ecEnv.ml                  |  69 +++++++++----
 src/ecEnv.mli                 |  24 ++++-
 src/ecHiGoal.ml               | 122 ++++++++++++++++++++++
 src/ecHiGoal.mli              |   1 +
 src/ecHiTacticals.ml          |  15 +++
 src/ecParser.mly              | 102 +++++++++++++++---
 src/ecParsetree.ml            |  38 ++++++-
 src/ecPrinting.ml             |  13 ++-
 src/ecReduction.ml            |  50 ++++++++-
 src/ecReduction.mli           |   3 +
 src/ecScope.ml                |   7 +-
 src/ecSimplifyContext.ml      | 112 ++++++++++++++++++++
 src/ecSimplifyContext.mli     |  41 ++++++++
 src/ecSubst.ml                |   9 +-
 src/ecTheory.ml               |   7 +-
 src/ecTheory.mli              |   7 +-
 src/ecTheoryReplay.ml         |   6 +-
 tests/hint_simplify_db.ec     |  21 ++++
 tests/local_hint_simplify.ec  | 169 ++++++++++++++++++++++++++++++
 tests/simplify_head_filter.ec |  58 +++++++++++
 24 files changed, 1041 insertions(+), 69 deletions(-)
 create mode 100644 doc/tactics/hint-simplify.rst
 create mode 100644 src/ecSimplifyContext.ml
 create mode 100644 src/ecSimplifyContext.mli
 create mode 100644 tests/hint_simplify_db.ec
 create mode 100644 tests/local_hint_simplify.ec
 create mode 100644 tests/simplify_head_filter.ec

diff --git a/doc/tactics/hint-simplify.rst b/doc/tactics/hint-simplify.rst
new file mode 100644
index 0000000000..7ffe5d4b0b
--- /dev/null
+++ b/doc/tactics/hint-simplify.rst
@@ -0,0 +1,188 @@
+========================================================================
+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.
+
+------------------------------------------------------------------------
+The `hint` clause
+------------------------------------------------------------------------
+
+`simplify` and `cbv` accept a single `hint` clause that controls which
+user-reduction rules are used. The clause is introduced by the `hint`
+keyword and is built from an unsigned base database selection followed by
+any number of signed items:
+
+.. admonition:: Syntax
+
+   `simplify hint {db}* {item}*`
+
+where each `{item}` is one of:
+
+- `+ {db}` / `- {db}` — activate / deactivate a database;
+- `+[ {op}+ ]` / `-[ {op}+ ]` — head filter: keep only / drop rules headed
+  by the listed operators (at most one filter per clause);
+- `{ {lemma}+ }` — add lemmas to the default database for this call.
+
+The delimiter disambiguates an item: a bare name is a database, `[…]`
+holds operators, `{…}` holds lemmas. Lemma sets are add-only -- a clause
+never removes lemmas from a database; use the head filter to restrict
+which rules apply. The same clause is accepted by `cbv`.
+
+The database part of a clause is *either* an unsigned selection *or*
+signed deltas, never both (mixing them is redundant and rejected). An
+unsigned list `hint d1 d2` **replaces** the consulted databases with
+exactly `{d1, d2}`. Signed `+ {db}` / `- {db}` instead modify the current
+set (the proof-local default, else the active set): `simplify hint +d2`
+adds `d2` to it, `simplify hint -d3` removes `d3`.
+
+A head filter performs full simplification (like a bare `simplify`) with
+user reduction restricted to the selected operators.
+
+The `hint` clause is independent of the reduction arguments that
+`simplify` and `cbv` already accept: a bare `simplify` performs full
+simplification, `simplify delta` additionally unfolds all definitions,
+`simplify f g` unfolds the operators `f` and `g`, and a keyword-less list
+such as `beta zeta` performs only the named reductions. A `hint` clause
+may follow any of these (for example `simplify delta hint +[f]`).
+
+------------------------------------------------------------------------
+Proof-local commands
+------------------------------------------------------------------------
+
+Inside a proof, the simplify configuration can be changed without
+modifying the theory-level declarations. The `hint` command takes the
+same clause as the `simplify`/`cbv` tactics, and each kind of item has a
+persistent effect on the proof state:
+
+.. admonition:: Syntax
+
+   `hint {db}* {item}* .`
+
+- `+ {db}` / `- {db}` — activate / deactivate a database (for later bare
+  `simplify`/`cbv`);
+- `{ {lemma}+ }` — add lemmas to the default database;
+- an unsigned database list `{db}+` — set the proof-local default
+  databases used by later `simplify`/`cbv` calls;
+- `+[ {op}+ ]` / `-[ {op}+ ]` — set the proof-local default head filter.
+
+As in the tactic clause, the database part is *either* an unsigned
+selection *or* signed `+`/`-` deltas, never both.
+
+.. admonition:: Syntax
+
+   `hint clear [ {db} ] .`
+
+Clear the local lemma additions (for the default database, or for
+`{db}`).
+
+.. admonition:: Syntax
+
+   `hint clear default .`
+
+Clear the proof-local default database and head filter.
+
+These proof-local changes are part of the proof state and therefore
+follow the usual subgoal branching behavior. Explicit arguments on
+`simplify`/`cbv` take precedence over the proof-local defaults.
+
+------------------------------------------------------------------------
+Scoped application
+------------------------------------------------------------------------
+
+A `hint` command can be used as a scoped wrapper around a tactic, with the
+same clause syntax.
+
+.. admonition:: Syntax
+
+   `with hint {clause} ( {tactic} )`
+
+For example:
+
+.. code-block:: easycrypt
+
+   with hint +ring (simplify).
+   with hint {fooE} (rewrite foo /=).
+   with 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 named (simplify).
+     trivial.
+   qed.
+
+   lemma demo_head_filter (x : int) :
+     box (wrap1 x) = box (x + 1).
+   proof.
+     simplify hint +[wrap1].
+     trivial.
+   qed.
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index 08f801623d..d25bd16587 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -322,18 +322,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
@@ -348,7 +341,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 4b75e5b0c1..ffe3874a82 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.simplify_context;       (* 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_simplify_context (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.SimplifyContext.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_simplify_context 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.SimplifyContext.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 f574b49bf3..90fe9bd98f 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.simplify_context;
 }
 
 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_simplify_context : tcenv1 -> EcEnv.simplify_context
 
   (* Low-level tactic markers *)
   val t_low0 : string -> backward -> backward
diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index 8a449a7797..39cd63260c 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,15 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Reduction = struct
+  type entry  = redentry
   type rule   = EcTheory.rule
   type topsym = red_topsym
+  type base = symbol
+
+  (* The default-database name is owned by [EcSimplifyContext]. *)
+  let dname : symbol = EcSimplifyContext.dname
 
-  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 +1514,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,28 +1525,48 @@ 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
 
+(* Proof-local simplify context lives in [EcSimplifyContext]; re-exported
+   here so client code can refer to [EcEnv.simplify_context] and
+   [EcEnv.SimplifyContext]. *)
+type simplify_context = EcSimplifyContext.simplify_context
+
+module SimplifyContext = EcSimplifyContext
+
 (* -------------------------------------------------------------------- *)
 module Auto = struct
   type base0 = path * [`Rigid | `Default]
@@ -3003,9 +3030,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 04354a391d..67b5cbb717 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -420,15 +420,29 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Reduction : sig
+  type entry = path * EcTheory.rule
   type rule   = EcTheory.rule
   type topsym = [ `Path of path | `Tuple | `Proj of int]
-
-  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
+  (* A reduction database is identified by a flat, global name (not a
+     theory-qualified path), hence a [symbol] rather than a [path]. *)
+  type base = symbol
+
+  (* Name of the default database (the empty name). *)
+  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
 
+(* Proof-local simplify context; defined in [EcSimplifyContext] and
+   re-exported here. *)
+type simplify_context = EcSimplifyContext.simplify_context
+
+module SimplifyContext = EcSimplifyContext
+
 (* -------------------------------------------------------------------- *)
 module Auto : sig
   type base0 = path * [`Rigid | `Default]
diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
index 5505e655fe..90668b2693 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_simplify_context tc in
+
+  let simpl =
+    match hint with
+    | PLHClause h ->
+        let opts = EcTheory.{ ur_delta = false; ur_eqtrue = false; } in
+
+        (* signed database deltas: [+d] activate, [-d] deactivate *)
+        let simpl =
+          List.fold_left (fun simpl (add, d) ->
+            if   add
+            then EcEnv.SimplifyContext.activate   [d] simpl
+            else EcEnv.SimplifyContext.deactivate [d] simpl)
+            simpl h.ph_dbs
+        in
+
+        (* lemma additions to the default DB (add-only) *)
+        let simpl =
+          List.fold_left (fun simpl lemma ->
+            let path = EcEnv.Ax.lookup_path (unloc lemma) env in
+            let rule = EcReduction.User.compile ~opts ~prio:0 env path in
+            EcEnv.SimplifyContext.add_rules [(path, rule)] simpl)
+            simpl h.ph_lemmas
+        in
+
+        (* an unsigned database list sets the proof-local default *)
+        let simpl =
+          match h.ph_select with
+          | [] -> simpl
+          | _  -> EcEnv.SimplifyContext.set_default_db h.ph_select simpl
+        in
+
+        (* a head filter sets the proof-local default head filter *)
+        let hd =
+          h.ph_hd |> 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
+        hd |> Option.fold ~none:simpl ~some:(fun hd ->
+          EcEnv.SimplifyContext.set_default_hd (Some hd) simpl)
+
+    | PLHClear base ->
+        EcEnv.SimplifyContext.clear ?base simpl
+
+    | PLHClearDefault ->
+        EcEnv.SimplifyContext.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_simplify_context tc in
 
   let do1 (sop, sid) ps =
     match ps.pl_desc with
@@ -113,6 +174,61 @@ let process_simplify_info ri (tc : tcenv1) =
       |> odfl ((fun _ -> `IfTransparent), predT)
   in
 
+  let hint = ri.phint in
+
+  (* Head filter: the clause filter if any, else the proof-local default. *)
+  let user_hd =
+    match hint.ph_hd with
+    | None -> EcEnv.SimplifyContext.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
+
+  (* Per-call lemma additions (add-only): compiled and applied to the
+     default DB of a local copy of the proof-local context. *)
+  let simpl =
+    let opts = EcTheory.{ ur_delta = false; ur_eqtrue = false; } in
+    List.fold_left (fun simpl lemma ->
+      let path = EcEnv.Ax.lookup_path (unloc lemma) env in
+      let rule = EcReduction.User.compile ~opts ~prio:0 env path in
+      EcEnv.SimplifyContext.add_rules [(path, rule)] simpl
+    ) simpl hint.ph_lemmas
+  in
+
+  (* Database list consulted by this call: the unsigned selection if any
+     (else the proof-local default / active set), with the signed
+     activate / deactivate deltas applied in order. [None] when no [hint]
+     clause is present, letting [EcReduction] use its own fallback. *)
+  let user_db =
+    if hint.ph_select = [] && hint.ph_dbs = [] then
+      None
+    else begin
+      let base =
+        if hint.ph_select <> [] then hint.ph_select else
+          match EcEnv.SimplifyContext.default_db simpl with
+          | Some dbs -> dbs
+          | None     -> EcSymbols.Ssym.elements (EcEnv.SimplifyContext.active simpl)
+      in
+      let dbs =
+        List.fold_left (fun dbs (add, d) ->
+          if add
+          then dbs @ [d]
+          else List.filter (fun d' -> d' <> d) dbs)
+          base hint.ph_dbs
+      in
+      Some dbs
+    end
+  in
+
   {
     EcReduction.beta    = ri.pbeta;
     EcReduction.delta_p = delta_p;
@@ -123,6 +239,12 @@ 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 = user_db;
+    EcReduction.user_local = simpl;
+    EcReduction.user_hd =
+      (match user_hd with
+       | Some _ as hd -> hd
+       | None -> EcEnv.SimplifyContext.default_hd simpl);
   }
 
 (*-------------------------------------------------------------------- *)
diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli
index 04220db14a..e6479da1ba 100644
--- a/src/ecHiGoal.mli
+++ b/src/ecHiGoal.mli
@@ -96,6 +96,7 @@ val process_congr       : pcongr_mode -> 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 0595c5d9e8..15095a323e 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -114,6 +114,19 @@ and process1_seq (ttenv : ttenv) (ts : ptactic list) (tc : tcenv1) =
 
   aux ts (tcenv_of_tcenv1 tc)
 
+(* -------------------------------------------------------------------- *)
+(* [with hint h (ts)]: run [ts] under the local hint command [h], then
+   restore the simplify context on all resulting subgoals. *)
+and process1_with (ttenv : ttenv) (h : plocalhint) (ts : ptactic list) (tc : tcenv1) =
+  let simpl = tc1_simplify_context 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
+
 (* -------------------------------------------------------------------- *)
 and process1_nstrict (ttenv : ttenv) (t : ptactic_core) (tc : tcenv1) =
   if ttenv.tt_smtmode <> `Strict then
@@ -156,6 +169,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 +342,7 @@ 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 (process1_with     ttenv h ts)
     | 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 95d9999e64..57d62459a4 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 ?(hint = empty_simplify_hint) l =
     if l = [] then
       { pbeta  = true; pzeta  = true;
         piota  = true; peta   = true;
         plogic = true; pdelta = None;
-        pmodpath = true; puser = true; }
+        pmodpath = true; puser = true; phint = hint; }
     else
       let doarg acc = function
         | `Delta l ->
@@ -113,7 +113,7 @@
           { pbeta  = false; pzeta  = false;
             piota  = false; peta   = false;
             plogic = false; pdelta = Some [];
-            pmodpath = false; puser = false; } l
+            pmodpath = false; puser = false; phint = hint; } l
 
   let simplify_red = [`Zeta; `Iota; `Beta; `Eta; `Logic; `ModPath; `User]
 
@@ -2490,6 +2490,9 @@ genpattern:
 | AT x=ident
     { `LetIn x }
 
+(* Bare reduction arguments, usable as a keyword-less tactic. The [+]/[-]
+   head filter is NOT allowed here: those tokens are bullet operators and
+   only a keyword ([simplify]/[cbv]) lets them be read as a head filter. *)
 simplify_arg:
 | DELTA l=qoident* { `Delta l }
 | ZETA             { `Zeta }
@@ -2499,16 +2502,70 @@ simplify_arg:
 | LOGIC            { `Logic }
 | MODPATH          { `ModPath }
 
+%inline pmode:
+| PLUS  { `Plus  }
+| MINUS { `Minus }
+
+(* One item of a [hint] clause: a database (bare name), a head filter
+   ([...]) or a lemma set ({...}); the delimiter disambiguates. The
+   structural constraints (single filter, selection vs deltas) are checked
+   in [simplify_hint_body]. *)
+simplify_hint_item:
+| m=pmode x=lident             { `Db    (m = `Plus, unloc x) }
+| m=pmode l=bracket(qoident+)  { `Hd    (m, l) }
+| l=brace(qident+)             { `Lemma l }
+
+(* The body of a [hint] clause: an unsigned base database selection
+   followed by items. A clause may not both select databases (unsigned
+   list) and use signed [+d]/[-d] deltas, and at most one head filter is
+   allowed. Lemma sets are add-only -- a clause never removes lemmas from
+   a database; use the head filter to restrict the rules that apply.
+   Shared by the [simplify]/[cbv] tactics and the proof-local commands. *)
+simplify_hint_body:
+| sel=lident* items=simplify_hint_item*
+    { let err msg = parse_error (EcLocation.make $startpos $endpos) (Some msg) in
+      let doit h = function
+        | `Db (b, d) -> { h with ph_dbs = h.ph_dbs @ [(b, d)] }
+        | `Hd (m, l) ->
+            if h.ph_hd <> None then err "a hint clause allows at most one head filter";
+            let m = match m with `Plus -> `Include | `Minus -> `Exclude in
+            { h with ph_hd = Some (m, l) }
+        | `Lemma l -> { h with ph_lemmas = h.ph_lemmas @ l }
+      in
+      let h =
+        List.fold_left doit
+          { empty_simplify_hint with ph_select = List.map unloc sel } items
+      in
+      if h.ph_select <> [] && h.ph_dbs <> [] then
+        err "a hint clause cannot mix a database selection with +/- database deltas";
+      h }
+
+(* A [hint] clause as used by the [simplify]/[cbv] tactics. *)
+simplify_hint:
+| HINT h=simplify_hint_body { h }
+
+(* Trailing modifier shared by every keyword [simplify]/[cbv] form: the
+   optional [hint] clause above. *)
+%inline simplify_mod:
+| c=simplify_hint? { odfl empty_simplify_hint c }
+
 simplify:
-| l=simplify_arg+     { l }
-| SIMPLIFY            { simplify_red }
-| SIMPLIFY l=qoident+ { `Delta l  :: simplify_red  }
-| SIMPLIFY DELTA      { `Delta [] :: simplify_red }
+| l=simplify_arg+
+    { mk_simplify l }
+| SIMPLIFY hint=simplify_mod
+    { mk_simplify ~hint simplify_red }
+| SIMPLIFY l=qoident+ hint=simplify_mod
+    { mk_simplify ~hint (`Delta l  :: simplify_red) }
+| SIMPLIFY DELTA hint=simplify_mod
+    { mk_simplify ~hint (`Delta [] :: simplify_red) }
 
 cbv:
-| CBV            { simplify_red }
-| CBV l=qoident+ { `Delta l  :: simplify_red  }
-| CBV DELTA      { `Delta [] :: simplify_red }
+| CBV hint=simplify_mod
+    { mk_simplify ~hint simplify_red }
+| CBV l=qoident+ hint=simplify_mod
+    { mk_simplify ~hint (`Delta l  :: simplify_red) }
+| CBV DELTA hint=simplify_mod
+    { mk_simplify ~hint (`Delta [] :: simplify_red) }
 
 conseq:
 | empty                            { None, None }
@@ -2795,6 +2852,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; } }
 
@@ -2892,10 +2952,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 }
@@ -3436,6 +3496,17 @@ caseoption:
 | n=word? NOT      { (`All, n) }
 | n=word? QUESTION { (`Maybe, n) }
 
+(* Proof-local simplify-hint commands, sharing the unified clause body
+   with the [simplify]/[cbv] tactics. *)
+localhint_cmd:
+| CLEAR d=lident?
+    { match omap unloc d with
+      | Some "default" -> PLHClearDefault
+      | base           -> PLHClear base }
+
+| h=simplify_hint_body
+    { PLHClause h }
+
 tactic_core_r:
 | IDTAC
    { Pidtac None }
@@ -3464,6 +3535,9 @@ tactic_core_r:
 | LPAREN s=tactics RPAREN
    { Pseq s }
 
+| WITH HINT h=localhint_cmd LPAREN s=tactics RPAREN
+   { Pwith (h, s) }
+
 | ADMIT
    { Padmit }
 
@@ -3908,8 +3982,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 8c2ccbadcb..b1d95a57d7 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -565,6 +565,25 @@ type pcutdef = {
 (* λ mem → formula *)
 type pmpred_args = (osymbol * pformula) list
 
+(* -------------------------------------------------------------------- *)
+(* The [hint …] clause of a [simplify]/[cbv] call. [ph_select] is the
+   unsigned base database selection (empty = use the proof-local default
+   / active set); [ph_dbs] are signed activate ([true]) / deactivate
+   ([false]) deltas on the current set; [ph_select] and [ph_dbs] are
+   mutually exclusive. [ph_hd] is the optional single-mode head filter;
+   [ph_lemmas] are lemmas added to the default DB for this call (lemma
+   sets are add-only -- the head filter restricts which rules apply). *)
+type psimplify_hint = {
+  ph_select : symbol list;
+  ph_dbs    : (bool * symbol) list;
+  ph_hd     : ([`Include | `Exclude] * pqsymbol list) option;
+  ph_lemmas : pqsymbol list;
+}
+
+let empty_simplify_hint = {
+  ph_select = []; ph_dbs = []; ph_hd = None; ph_lemmas = [];
+}
+
 (* -------------------------------------------------------------------- *)
 type preduction = {
   pbeta    : bool;                      (* β-reduction *)
@@ -575,6 +594,7 @@ type preduction = {
   plogic   : bool;                      (* logical simplification *)
   pmodpath : bool;                      (* modpath normalization *)
   puser    : bool;                      (* user reduction *)
+  phint    : psimplify_hint;            (* use-site [hint …] clause *)
 }
 
 (* -------------------------------------------------------------------- *)
@@ -1052,6 +1072,20 @@ type pcongr_mode =
   | PCongrStar
   | PCongrPattern of pformula
 
+(* -------------------------------------------------------------------- *)
+type phintdbmode = [ `Add | `Remove ]
+
+(* A proof-local simplify-hint command. [PLHClause] applies a unified
+   [hint] clause: signed [+d]/[-d] activate/deactivate databases, signed
+   lemma sets [+{L}]/[-{L}] add/remove local lemmas (default DB), an
+   unsigned database list sets the proof-local default databases, and a
+   [+[ops]]/[-[ops]] filter sets the proof-local default head filter.
+   [PLHClear] / [PLHClearDefault] reset the local lemmas / the defaults. *)
+type plocalhint =
+  | PLHClause of psimplify_hint
+  | PLHClear of symbol option
+  | PLHClearDefault
+
 (* -------------------------------------------------------------------- *)
 type logtactic =
   | Preflexivity
@@ -1083,6 +1117,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 =
@@ -1099,6 +1134,7 @@ and ptactic_core_r =
   | Pprogress   of ppgoptions * ptactic_core option
   | Psubgoal    of ptactic_chain
   | Pnstrict    of ptactic_core
+  | Pwith       of plocalhint * ptactics
   | Padmit
 
 (* -------------------------------------------------------------------- *)
@@ -1339,7 +1375,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 b5f4e20300..202e540b32 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -3834,9 +3834,16 @@ 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 _ ->
-      (* FIXME: section we should add the lemma in the reduction *)
-      Format.fprintf fmt "hint simplify."
+  | EcTheory.Th_reduction { red_base; red_rules; } ->
+      (* [hint simplify <lemmas>.] for the default base; [hint simplify in
+         <base> : <lemmas>.] for a named one (mirrors the grammar). *)
+      let pp_head fmt = function
+        | None      -> Format.fprintf fmt "hint simplify"
+        | Some base -> Format.fprintf fmt "hint simplify in %s :" base in
+      let lemmas = List.map proj3_1 red_rules in
+      Format.fprintf fmt "%a @[<hov 2>%a@]."
+        pp_head red_base
+        (pp_list ",@ " (pp_axname ppe)) lemmas
 
   | 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 d28cb2058c..8575fb3f8e 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -642,6 +642,12 @@ type reduction_info = {
   logic   : rlogic_info;
   modpath : bool;
   user    : bool;
+  (* Databases selected at the use-site: [None] = no explicit selection
+     (fall back to the proof-local context), [Some dbs] = use exactly
+     [dbs] (replacing the active set). *)
+  user_db : EcSymbols.symbol list option;
+  user_local : EcEnv.simplify_context;
+  user_hd : EcEnv.SimplifyContext.head_filter option;
 }
 
 and deltap      = [Op.redmode | `No]
@@ -658,6 +664,9 @@ let full_red = {
   logic   = Some `Full;
   modpath = true;
   user    = true;
+  user_db = None;
+  user_local = EcEnv.SimplifyContext.empty;
+  user_hd = None;
 }
 
 let no_red = {
@@ -670,6 +679,9 @@ let no_red = {
   logic   = None;
   modpath = false;
   user    = false;
+  user_db = None;
+  user_local = EcEnv.SimplifyContext.empty;
+  user_hd = None;
 }
 
 let beta_red     = { no_red with beta = true; }
@@ -741,8 +753,44 @@ 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 rules =
+      EcEnv.Reduction.get_entries ~base p env
+      |> List.map snd
+    in
+    let added =
+      EcEnv.SimplifyContext.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
+
+  (* Use-site selection replaces the active set; otherwise fall back to
+     the proof-local default databases, then to the active set. *)
+  let bases =
+    match ri.user_db with
+    | Some dbs -> dbs
+    | None ->
+        match EcEnv.SimplifyContext.default_db ri.user_local with
+        | Some dbs -> dbs
+        | None -> EcSymbols.Ssym.elements (EcEnv.SimplifyContext.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 ceb057d245..7abd035629 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 list option; (* use-site database selection *)
+  user_local : EcEnv.simplify_context; (* proof-local simplify overlay *)
+  user_hd : EcEnv.SimplifyContext.head_filter option; (* head filter *)
 }
 
 and deltap      = [EcEnv.Op.redmode | `No]
diff --git a/src/ecScope.ml b/src/ecScope.ml
index c6f1ff7fdb..b8bd23b88c 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -2093,7 +2093,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 =
@@ -2114,7 +2114,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/ecSimplifyContext.ml b/src/ecSimplifyContext.ml
new file mode 100644
index 0000000000..39c90e1a02
--- /dev/null
+++ b/src/ecSimplifyContext.ml
@@ -0,0 +1,112 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcSymbols
+open EcPath
+
+(* -------------------------------------------------------------------- *)
+type entry = path * EcTheory.rule
+
+(* A head filter restricts user-reduction rules to (or away from) those
+   whose left-hand side is headed by one of the given symbols. *)
+type head_mode = [`Include | `Exclude]
+type head_filter = [`Include of Sp.t | `Exclude of Sp.t]
+
+(* Canonical name of the default simplify database. A database is named
+   by a [symbol]; the default one carries the empty name. This is the
+   single source for that name, re-exported as [EcEnv.Reduction.dname]. *)
+let dname : symbol = ""
+
+(* -------------------------------------------------------------------- *)
+type simplify_context = {
+  (* Names of the databases currently active for a bare [simplify]/[cbv]
+     (always contains [dname]). *)
+  ls_active     : Ssym.t;
+  (* Proof-local default databases consulted by later bare [simplify]/
+     [cbv] calls: [None] = no local default (fall back to [ls_active]),
+     [Some dbs] = use exactly [dbs]. *)
+  ls_default_db : symbol list option;
+  (* Proof-local default head filter, similarly overriding the absence of
+     an explicit filter on [simplify]/[cbv]. *)
+  ls_default_hd : head_filter option;
+  (* Per-database overlay of locally added rules (add-only). *)
+  ls_added      : entry list Msym.t;
+}
+
+(* -------------------------------------------------------------------- *)
+let empty : simplify_context = {
+  ls_active     = Ssym.singleton dname;
+  ls_default_db = None;
+  ls_default_hd = None;
+  ls_added      = Msym.empty;
+}
+
+(* -------------------------------------------------------------------- *)
+let active (ls : simplify_context) : Ssym.t =
+  ls.ls_active
+
+(* -------------------------------------------------------------------- *)
+let default_db (ls : simplify_context) : symbol list option =
+  ls.ls_default_db
+
+(* -------------------------------------------------------------------- *)
+let default_hd (ls : simplify_context) : head_filter option =
+  ls.ls_default_hd
+
+(* -------------------------------------------------------------------- *)
+(* [None] denotes the default database. *)
+let normbase (base : symbol option) : symbol =
+  odfl dname base
+
+(* -------------------------------------------------------------------- *)
+let activate (bases : symbol list) (ls : simplify_context) : simplify_context =
+  { ls with ls_active = List.fold_left (fun st b -> Ssym.add b st) ls.ls_active bases }
+
+(* -------------------------------------------------------------------- *)
+let deactivate (bases : symbol list) (ls : simplify_context) : simplify_context =
+  { ls with ls_active = List.fold_left (fun st b -> Ssym.remove b st) ls.ls_active bases }
+
+(* -------------------------------------------------------------------- *)
+let set_default_db (bases : symbol list) (ls : simplify_context) : simplify_context =
+  { ls with ls_default_db = Some bases }
+
+(* -------------------------------------------------------------------- *)
+let set_default_hd
+  (hd : (head_mode * path list) option)
+  (ls : simplify_context)
+  : simplify_context
+=
+  let hd = hd |> omap (fun (mode, paths) ->
+    match mode with
+    | `Include -> `Include (Sp.of_list paths)
+    | `Exclude -> `Exclude (Sp.of_list paths))
+  in
+  { ls with ls_default_hd = hd }
+
+(* -------------------------------------------------------------------- *)
+let clear_default (ls : simplify_context) : simplify_context =
+  { ls with ls_default_db = None; ls_default_hd = None }
+
+(* -------------------------------------------------------------------- *)
+let added ?(base : symbol option) (ls : simplify_context) : entry list =
+  Msym.find_def [] (normbase base) ls.ls_added
+
+(* -------------------------------------------------------------------- *)
+let add_rules
+  ?(base  : symbol option)
+   (rules : entry list)
+   (ls    : simplify_context)
+  : simplify_context
+=
+  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
+  { ls with ls_added = Msym.add base (old @ rules) ls.ls_added }
+
+(* -------------------------------------------------------------------- *)
+let clear ?(base : symbol option) (ls : simplify_context) : simplify_context =
+  let base = normbase base in
+  { ls with ls_added = Msym.remove base ls.ls_added }
diff --git a/src/ecSimplifyContext.mli b/src/ecSimplifyContext.mli
new file mode 100644
index 0000000000..cf541a1cee
--- /dev/null
+++ b/src/ecSimplifyContext.mli
@@ -0,0 +1,41 @@
+(* -------------------------------------------------------------------- *)
+open EcSymbols
+open EcPath
+
+(* -------------------------------------------------------------------- *)
+(* Proof-local simplify context: the set of active simplify databases,
+   proof-local defaults (database / head filter) and the per-database
+   overlay of locally added user-reduction rules. *)
+
+type entry = path * EcTheory.rule
+
+(* A head filter restricts user-reduction rules to (or away from) those
+   whose left-hand side is headed by one of the given symbols. *)
+type head_mode = [`Include | `Exclude]
+type head_filter = [`Include of Sp.t | `Exclude of Sp.t]
+
+(* Canonical name of the default simplify database (the empty name). *)
+val dname : symbol
+
+type simplify_context
+
+val empty : simplify_context
+
+val active : simplify_context -> Ssym.t
+(* Proof-local default databases for bare [simplify]/[cbv]: [None] means
+   no local default, [Some dbs] means consult exactly [dbs]. *)
+val default_db : simplify_context -> symbol list option
+val default_hd : simplify_context -> head_filter option
+
+val activate : symbol list -> simplify_context -> simplify_context
+val deactivate : symbol list -> simplify_context -> simplify_context
+
+val set_default_db : symbol list -> simplify_context -> simplify_context
+val set_default_hd :
+  (head_mode * path list) option -> simplify_context -> simplify_context
+val clear_default : simplify_context -> simplify_context
+
+val added : ?base:symbol -> simplify_context -> entry list
+
+val add_rules : ?base:symbol -> entry list -> simplify_context -> simplify_context
+val clear : ?base:symbol -> simplify_context -> simplify_context
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index 2faa406794..1ec8709f98 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -1067,10 +1067,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 =
@@ -1215,4 +1215,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 c4bcbfe19c..5f6e375f15 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 20c34364b8..2a59ff246c 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 234a56d3a5..18dd239080 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -939,7 +939,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
@@ -958,8 +958,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 0000000000..24f93b9949
--- /dev/null
+++ b/tests/hint_simplify_db.ec
@@ -0,0 +1,21 @@
+require import Int.
+
+(* Abstract operators reduced only by the rules below; the named rule
+   lives outside the default DB so closing the goal genuinely depends on
+   [simplify] firing the rule (see tests/local_hint_simplify.ec). *)
+op wrap_default : int -> int.
+op wrap_named : 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) :
+  wrap_default x = x + 1.
+proof. simplify. done. qed.
+
+lemma wrap_named_simplifies (x : int) :
+  wrap_named x = x + 2.
+proof. simplify hint named. done. qed.
diff --git a/tests/local_hint_simplify.ec b/tests/local_hint_simplify.ec
new file mode 100644
index 0000000000..b12ab0dd48
--- /dev/null
+++ b/tests/local_hint_simplify.ec
@@ -0,0 +1,169 @@
+require import Int.
+
+(* Abstract operators (no body) so only the user-reduction rules below can
+   reduce them. Rules headed by these ops are placed in named DBs (not the
+   default one) so kernel conversion never applies them implicitly; a goal
+   closes only when [simplify] actually fires the rule. That makes the
+   [fail (...)] phrases below faithful witnesses that a disabled rule does
+   nothing. *)
+op foo : int -> int.   (* default DB        *)
+op bar : int -> int.   (* named DB [dbA]    *)
+op baz : int -> int.   (* named DB [dbB]    *)
+op qux : int -> int.   (* added locally     *)
+
+axiom fooE (x : int) : foo x = x + 1.
+axiom barE (x : int) : bar x = x + 2.
+axiom bazE (x : int) : baz x = x + 3.
+axiom quxE (x : int) : qux x = x + 4.
+
+hint simplify fooE.
+hint simplify in dbA : barE.
+hint simplify in dbB : bazE.
+
+(* --- Named-database selection (E1) ----------------------------------- *)
+
+lemma select_named_db (x : int) :
+  bar x = x + 2.
+proof. simplify hint dbA. done. qed.
+
+(* Several databases can be selected at once. *)
+lemma select_multiple_dbs (x : int) :
+  bar x = x + 2 /\ baz x = x + 3.
+proof. simplify hint dbA dbB. split; done. qed.
+
+(* Selection *replaces* the active set: naming [dbA] consults only [dbA],
+   so a rule from the unselected [dbB] does not fire and its goal cannot
+   close until [dbB] is selected too. *)
+lemma selection_replaces_active (x : int) :
+  baz x = x + 3.
+proof.
+  fail (simplify hint dbA; done).
+  simplify hint dbB.
+  done.
+qed.
+
+(* Signed [+d] deltas add databases to the active set for this call
+   (no unsigned base: a clause is either a selection or deltas). *)
+lemma activate_deltas (x : int) :
+  bar x = x + 2 /\ baz x = x + 3.
+proof. simplify hint +dbA +dbB. split; done. qed.
+
+(* A [-d] delta removes a database; [-dbB] drops [dbB] so its rule no
+   longer fires, until it is added again. *)
+lemma deactivate_delta (x : int) :
+  baz x = x + 3.
+proof.
+  fail (simplify hint +dbA +dbB -dbB; done).
+  simplify hint +dbB.
+  done.
+qed.
+
+(* Per-call lemma add via [{ ... }] (targets the default DB), without a
+   persistent [hint] command. *)
+lemma per_call_lemma_add (x : int) :
+  qux x = x + 4.
+proof.
+  fail (simplify; done).
+  simplify hint {quxE}.
+  done.
+qed.
+
+(* --- Activating / deactivating databases ----------------------------- *)
+
+lemma activate_named_db (x : int) :
+  bar x = x + 2.
+proof.
+  hint +dbA.
+  simplify.
+  done.
+qed.
+
+(* Deactivating a previously-activated DB must disable its rules again. *)
+lemma deactivate_named_db (x : int) :
+  bar x = x + 2.
+proof.
+  hint +dbA.
+  hint -dbA.
+  fail (simplify; done).
+  hint +dbA.
+  simplify.
+  done.
+qed.
+
+(* --- Local lemma add / remove / clear -------------------------------- *)
+
+lemma add_local_hint (x : int) :
+  qux x = x + 4.
+proof.
+  hint {quxE}.
+  simplify.
+  done.
+qed.
+
+(* [hint clear] drops the local additions, disabling the lemma again. *)
+lemma clear_local_hints (x : int) :
+  qux x = x + 4.
+proof.
+  hint {quxE}.
+  hint clear.
+  fail (simplify; done).
+  hint {quxE}.
+  simplify.
+  done.
+qed.
+
+(* --- Scoped application: [with hint cmd (tac)] ----------------------- *)
+
+lemma scoped_with_hint_db (x : int) :
+  bar x = x + 2.
+proof. with hint +dbA (simplify). done. qed.
+
+lemma scoped_with_hint_lemma (x : int) :
+  qux x = x + 4.
+proof. with hint {quxE} (simplify). done. qed.
+
+(* The scoped configuration is restored afterwards: the local add applies
+   only inside the wrapped tactic. Here the wrapper just runs [split]; the
+   resulting subgoals no longer see the added rule, so each one must
+   re-add it to close. *)
+lemma scoped_with_hint_restores (x : int) :
+  qux x = x + 4 /\ qux x = x + 4.
+proof.
+  with hint {quxE} (split).
+  fail (simplify; done).
+  hint {quxE}; simplify; done.
+  hint {quxE}; simplify; done.
+qed.
+
+(* --- Proof-local defaults -------------------------------------------- *)
+
+lemma local_default_db (x : int) :
+  bar x = x + 2.
+proof.
+  hint dbA.
+  simplify.
+  done.
+qed.
+
+lemma scoped_default_db (x : int) :
+  bar x = x + 2.
+proof. with hint dbA (simplify). done. qed.
+
+lemma local_default_head_filter (x : int) :
+  qux x = x + 4.
+proof.
+  hint {quxE}.
+  hint +[qux].
+  simplify.
+  done.
+qed.
+
+(* Clearing the local default reverts to the active set. *)
+lemma clear_local_default (x : int) :
+  bar x = x + 2.
+proof.
+  hint dbA.
+  hint clear default.
+  simplify hint dbA.
+  done.
+qed.
diff --git a/tests/simplify_head_filter.ec b/tests/simplify_head_filter.ec
new file mode 100644
index 0000000000..9a13a2892a
--- /dev/null
+++ b/tests/simplify_head_filter.ec
@@ -0,0 +1,58 @@
+require import Int.
+
+(* [foo]/[bar] are abstract: they have no body, so nothing reduces them
+   except the user-reduction rules below. The rules live in a *named* DB
+   (not the default one), so kernel conversion never applies them on its
+   own -- a goal closes only when [simplify] actually fires the rule.
+   This lets [fail (...)] witness that a filtered-out rule does nothing. *)
+op foo : int -> int.
+op bar : int -> int.
+op baz : int -> int.
+
+axiom fooE (x : int) : foo x = x + 1.
+axiom barE (x : int) : bar x = x + 2.
+axiom bazE (x : int) : baz x = x + 3.
+
+hint simplify in mydb : fooE.
+hint simplify in mydb : barE.
+hint simplify bazE.            (* default (active) DB *)
+
+(* Include filter: only [foo]-headed rules fire. *)
+lemma simplify_include (x : int) :
+  foo x = x + 1.
+proof. simplify hint mydb +[foo]. done. qed.
+
+(* Exclude filter: every rule except the [bar]-headed ones fires, so
+   [foo] still reduces. *)
+lemma simplify_exclude (x : int) :
+  foo x = x + 1.
+proof. simplify hint mydb -[bar]. done. qed.
+
+(* The excluded rule genuinely does nothing: with [foo] filtered out the
+   goal cannot be closed, but it can once [foo] is included again. *)
+lemma simplify_exclude_disables (x : int) :
+  foo x = x + 1.
+proof.
+  fail (simplify hint mydb -[foo]; done).
+  simplify hint mydb +[foo].
+  done.
+qed.
+
+(* A head filter with no named database filters over the active set
+   (the [hint] keyword is mandatory, the database list may be empty). *)
+lemma simplify_filter_active_set (x : int) :
+  baz x = x + 3.
+proof. simplify hint +[baz]. done. qed.
+
+(* Head filters combine with [cbv] the same way. *)
+lemma cbv_include (x : int) :
+  bar x = x + 2.
+proof. cbv hint mydb +[bar]. done. qed.
+
+lemma cbv_exclude_disables (x : int) :
+  bar x = x + 2.
+proof.
+  fail (cbv hint mydb -[bar]; done).
+  cbv hint mydb +[bar].
+  done.
+qed.