diff --git a/src/ecDecl.ml b/src/ecDecl.ml
index 5806407fa..c22745a78 100644
--- a/src/ecDecl.ml
+++ b/src/ecDecl.ml
@@ -16,10 +16,9 @@ type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_resolve : bool;
+  tyd_params : ty_params;
+  tyd_type   : ty_body;
+  tyd_loca   : locality;
 }
 
 and ty_body = [
@@ -48,7 +47,7 @@ let tydecl_as_record (td : tydecl) =
   match td.tyd_type with `Record x -> Some x | _ -> None
 
 (* -------------------------------------------------------------------- *)
-let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
+let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
   let params =
     match params with
     | `Named params ->
@@ -60,7 +59,7 @@ let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
           (EcUid.NameGen.bulk ~fmt n)
   in
 
-  { tyd_params = params; tyd_type = `Abstract tc; tyd_resolve = resolve; tyd_loca = lc; }
+  { tyd_params = params; tyd_type = `Abstract tc; tyd_loca = lc; }
 
 (* -------------------------------------------------------------------- *)
 let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =
@@ -137,13 +136,11 @@ and opopaque = { smt: bool; reduction: bool; }
 type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
 
 type axiom = {
-  ax_tparams    : ty_params;
-  ax_spec       : EcCoreFol.form;
-  ax_kind       : axiom_kind;
-  ax_loca       : locality;
-  ax_visibility : ax_visibility; }
-
-and ax_visibility = [`Visible | `NoSmt | `Hidden]
+  ax_tparams : ty_params;
+  ax_spec    : EcCoreFol.form;
+  ax_kind    : axiom_kind;
+  ax_loca    : locality;
+  ax_smt     : bool; }
 
 let is_axiom  (x : axiom_kind) = match x with `Axiom _ -> true | _ -> false
 let is_lemma  (x : axiom_kind) = match x with `Lemma   -> true | _ -> false
@@ -272,11 +269,11 @@ let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc =
   let op     = f_app op opargs axbd.f_ty in
   let axspec = f_forall args (f_eq op axbd) in
 
-  { ax_tparams    = axpm;
-    ax_spec       = axspec;
-    ax_kind       = `Axiom (Ssym.empty, false);
-    ax_loca       = lc;
-    ax_visibility = if nosmt then `NoSmt else `Visible; }
+  { ax_tparams = axpm;
+    ax_spec    = axspec;
+    ax_kind    = `Axiom (Ssym.empty, false);
+    ax_loca    = lc;
+    ax_smt     = not nosmt; }
 
 (* -------------------------------------------------------------------- *)
 type typeclass = {
diff --git a/src/ecDecl.mli b/src/ecDecl.mli
index 65e2dea27..6bde7e114 100644
--- a/src/ecDecl.mli
+++ b/src/ecDecl.mli
@@ -12,10 +12,9 @@ type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_resolve : bool;
+  tyd_params : ty_params;
+  tyd_type   : ty_body;
+  tyd_loca   : locality;
 }
 
 and ty_body = [
@@ -36,7 +35,7 @@ val tydecl_as_abstract : tydecl -> Sp.t option
 val tydecl_as_datatype : tydecl -> ty_dtype option
 val tydecl_as_record   : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list) option
 
-val abs_tydecl : ?resolve:bool -> ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
+val abs_tydecl : ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
 
 val ty_instanciate : ty_params -> ty list -> ty -> ty
 
@@ -135,15 +134,13 @@ val operator_as_prind : operator -> prind
 type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
 
 type axiom = {
-  ax_tparams    : ty_params;
-  ax_spec       : form;
-  ax_kind       : axiom_kind;
-  ax_loca       : locality;
-  ax_visibility : ax_visibility;
+  ax_tparams : ty_params;
+  ax_spec    : form;
+  ax_kind    : axiom_kind;
+  ax_loca    : locality;
+  ax_smt     : bool;
 }
 
-and ax_visibility = [`Visible | `NoSmt | `Hidden]
-
 (* -------------------------------------------------------------------- *)
 val is_axiom  : axiom_kind -> bool
 val is_lemma  : axiom_kind -> bool
diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index a83045d38..011c71234 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -739,11 +739,11 @@ module MC = struct
       let axp  = EcPath.prefix (Lazy.force mypath) in
       let axp  = IPPath (EcPath.pqoname axp name) in
       let ax   =
-        { ax_kind       = `Lemma;
-          ax_tparams    = tv;
-          ax_spec       = cl;
-          ax_loca       = (snd obj).op_loca;
-          ax_visibility = `Visible; } in
+        { ax_kind    = `Lemma;
+          ax_tparams = tv;
+          ax_spec    = cl;
+          ax_loca    = (snd obj).op_loca;
+          ax_smt     = true; } in
       (name, (axp, ax))) ax in
 
     List.fold_left (fun mc -> curry (_up_axiom candup mc)) mc ax
@@ -795,13 +795,11 @@ module MC = struct
           let (schelim, schcase) =
             let do1 scheme name =
               let scname = Printf.sprintf "%s_%s" x name in
-                (scname, { ax_tparams    = tyd.tyd_params;
-                           ax_spec       = scheme;
-                           ax_kind       = `Lemma;
-                           ax_loca       = loca;
-                           ax_visibility = `NoSmt;
-                })
-            in
+                (scname, { ax_tparams = tyd.tyd_params;
+                           ax_spec    = scheme;
+                           ax_kind    = `Lemma;
+                           ax_loca    = loca;
+                           ax_smt     = false; }) in
               (do1 schelim "ind", do1 schcase "case")
           in
 
@@ -840,12 +838,11 @@ module MC = struct
 
           let scheme =
             let scname = Printf.sprintf "%s_ind" x in
-              (scname, { ax_tparams    = tyd.tyd_params;
-                         ax_spec       = scheme;
-                         ax_kind       = `Lemma;
-                         ax_loca       = loca;
-                         ax_visibility = `NoSmt;
-              })
+              (scname, { ax_tparams = tyd.tyd_params;
+                         ax_spec    = scheme;
+                         ax_kind    = `Lemma;
+                         ax_loca    = loca;
+                         ax_smt     = false; })
           in
 
           let stname = Printf.sprintf "mk_%s" x in
@@ -927,11 +924,11 @@ module MC = struct
         List.map
           (fun (x, ax) ->
             let ax = EcSubst.subst_form fsubst ax in
-              (x, { ax_tparams    = [(self, Sp.singleton mypath)];
-                    ax_spec       = ax;
-                    ax_kind       = `Lemma;
-                    ax_loca       = loca;
-                    ax_visibility = `NoSmt; }))
+              (x, { ax_tparams = [(self, Sp.singleton mypath)];
+                    ax_spec    = ax;
+                    ax_kind    = `Lemma;
+                    ax_loca    = loca;
+                    ax_smt     = false; }))
           tc.tc_axs
       in
 
@@ -1369,10 +1366,10 @@ module TypeClass = struct
           let myself = EcPath.pqname (root env) name in
             { env with env_tc = TC.Graph.add ~src:myself ~dst:prt env.env_tc }
 
-  let bind ?(import = import0) name tc env =
-    let env = if import.im_immediate then rebind name tc env else env in
-    { env with
-        env_item = mkitem import (Th_typeclass (name, tc)) :: env.env_item }
+  let bind ?(import = true) name tc env =
+    let env = rebind name tc env in
+    let item = Th_typeclass (name, tc) in
+    { env with env_item = mkitem ~import item :: env.env_item }
 
   let lookup qname (env : env) =
     MC.lookup_typeclass qname env
@@ -1389,14 +1386,11 @@ module TypeClass = struct
   let bind_instance ty cr tci =
     (ty, cr) :: tci
 
-  let add_instance ?(import = import0) ty cr lc env =
-    let env =
-      if import.im_immediate then
-        { env with env_tci = bind_instance ty cr env.env_tci }
-      else env in
+  let add_instance ?(import = true) ty cr lc env =
+    let item = Th_instance (ty, cr, lc) in
     { env with
         env_tci  = bind_instance ty cr env.env_tci;
-        env_item = mkitem import (Th_instance (ty, cr, lc)) :: env.env_item; }
+        env_item = mkitem ~import item :: env.env_item; }
 
   let get_instances env = env.env_tci
 end
@@ -1427,30 +1421,21 @@ module BaseRw = struct
     | None -> false
     | Some _ -> true
 
-  let add ?(import = import0) name lc env =
+  let add ?(import = true) name lc env =
     let p   = EcPath.pqname (root env) name in
-    let env = if import.im_immediate then MC.bind_rwbase name p env else env in
+    let env = MC.bind_rwbase name p env in
     let ip  = IPPath p in
     { env with
         env_rwbase = Mip.add ip Sp.empty env.env_rwbase;
-        env_item   = mkitem import (Th_baserw (name, lc)) :: env.env_item; }
-
-  let addto ?(import = import0) p l lc env =
-    let env =
-      if import.im_immediate then
-        { env with
-            env_rwbase =
-              Mip.change
-                (omap (fun s -> List.fold_left (fun s r -> Sp.add r s) s l))
-                (IPPath p) env.env_rwbase }
-      else env in
+        env_item   = mkitem ~import (Th_baserw (name, lc)) :: env.env_item; }
 
+  let addto ?(import = true) p l lc env =
     { env with
         env_rwbase =
           Mip.change
             (omap (fun s -> List.fold_left (fun s r -> Sp.add r s) s l))
             (IPPath p) env.env_rwbase;
-        env_item = mkitem import (Th_addrw (p, l, lc)) :: env.env_item; }
+        env_item = mkitem ~import (Th_addrw (p, l, lc)) :: env.env_item; }
 
   let all env =
     List.filter_map (fun (ip, sp) -> 
@@ -1493,15 +1478,12 @@ module Reduction = struct
   let add_rules (rules : (path * rule option) list) (db : mredinfo) =
     List.fold_left ((^~) add_rule) db rules
 
-  let add ?(import = import0) (rules : (path * rule_option * rule option) list) (env : env) =
+  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 env =
-      if import.im_immediate then
-        { env with env_redbase = add_rules rstrip env.env_redbase; }
-      else env in
 
     { env with
-        env_item = mkitem import (Th_reduction rules) :: env.env_item; }
+        env_redbase = add_rules rstrip env.env_redbase;
+        env_item = mkitem ~import (Th_reduction rules) :: env.env_item; }
 
   let add1 (prule : path * rule_option * rule option) (env : env) =
     add [prule] env
@@ -1538,21 +1520,17 @@ module Auto = struct
     Msym.add nbase levels db
 
   let add
-    ?(import   = import0)
+    ?(import   = true)
     ~(level    : int)
     ?(base     : symbol option)
      (axioms   : atbase0 list)
      (locality : is_local)
      (env      : env)
   =
-    let env =
-      if import.im_immediate then
-        { env with
-            env_atbase = updatedb ?base ~level axioms env.env_atbase; }
-      else env
-    in
-      { env with env_item = mkitem import
-         (Th_auto { level; base; axioms; locality; }) :: env.env_item; }
+    let item = Th_auto { level; base; axioms; locality; } in
+    { env with
+        env_atbase = updatedb ?base ~level axioms env.env_atbase;
+        env_item = mkitem ~import item :: env.env_item; }
 
   let add1 ?import ~level ?base (p : atbase0) lc (env : env) =
     add ?import ?base ~level [p] lc env
@@ -1983,12 +1961,12 @@ module Mod = struct
       add_xs_to_declared xs env
     else env
 
-  let bind ?(import = import0) name me env =
+  let bind ?(import = true) name me env =
     assert (name = me.tme_expr.me_name);
-    let env = if import.im_immediate then MC.bind_mod name me env else env in
+    let env = MC.bind_mod name me env in
     let env =
       { env with
-          env_item = mkitem import (Th_module me) :: env.env_item;
+          env_item = mkitem ~import (Th_module me) :: env.env_item;
           env_norm = ref !(env.env_norm); } in
     add_restr_to_declared (root env) me env
 
@@ -2113,10 +2091,10 @@ module ModTy = struct
       mt_name   = p;
       mt_args   = List.map (EcPath.mident -| fst) sig_.mis_params; }
 
-  let bind ?(import = import0) name modty env =
-    let env = if import.im_immediate then MC.bind_modty name modty env else env in
-      { env with
-          env_item = mkitem import (Th_modtype (name, modty)) :: env.env_item }
+  let bind ?(import = true) name modty env =
+    let env = MC.bind_modty name modty env in
+    { env with
+        env_item = mkitem ~import (Th_modtype (name, modty)) :: env.env_item }
 
   let sig_of_mt (env : env) (mt : module_type) : module_sig =
     let { tms_sig = sig_ } = by_path mt.mt_name env in
@@ -2607,11 +2585,10 @@ module Ty = struct
 
     | _ -> env
 
-  let bind ?(import = import0) name ty env =
-    let env = if import.im_immediate then rebind name ty env else env in
+  let bind ?(import = true) name ty env =
+    let env = rebind name ty env in
     { env with env_item =
-        mkitem import (Th_type (name, ty)) :: env.env_item }
-
+        mkitem ~import (Th_type (name, ty)) :: env.env_item }
 
   let iter ?name f (env : env) =
     gen_iter (fun mc -> mc.mc_tydecls) MC.lookup_tydecls ?name f env
@@ -2670,13 +2647,11 @@ module Op = struct
         Mop.change (fun nts -> Some (nt :: odfl [] nts)) hd nts)
       base nt
 
-  let bind ?(import = import0) name op env =
-    let env = if import.im_immediate then MC.bind_operator name op env else env in
-    let env_ntbase = update_ntbase (root env) (name, op) env.env_ntbase in
-
+  let bind ?(import = true) name op env =
+    let env = MC.bind_operator name op env in
     { env with
-        env_ntbase;
-        env_item = mkitem import (Th_operator (name, op)) :: env.env_item; }
+        env_ntbase = update_ntbase (root env) (name, op) env.env_ntbase;
+        env_item = mkitem ~import (Th_operator (name, op)) :: env.env_item; }
 
   let rebind name op env =
     MC.bind_operator name op env
@@ -2795,9 +2770,9 @@ module Ax = struct
   let lookup_path name env =
     fst (lookup name env)
 
-  let bind ?(import = import0) name ax env =
-    let env = if import.im_immediate then MC.bind_axiom name ax env else env in
-    { env with env_item = mkitem import (Th_axiom (name, ax)) :: env.env_item }
+  let bind ?(import = true) name ax env =
+    let env = MC.bind_axiom name ax env in
+    { env with env_item = mkitem ~import (Th_axiom (name, ax)) :: env.env_item }
 
   let rebind name ax env =
     MC.bind_axiom name ax env
@@ -2891,7 +2866,7 @@ module Theory = struct
     List.fold_left (bind_instance_th_item path) inst cth
 
   and bind_instance_th_item path inst item =
-    if not item.ti_import.im_atimport then inst else
+    if not item.ti_import then inst else
 
     let xpath x = EcPath.pqname path x in
 
@@ -2923,7 +2898,7 @@ module Theory = struct
     List.fold_left (bind_base_th_item tx path) base cth
 
   and bind_base_th_item tx path base item =
-    if not item.ti_import.im_atimport then base else
+    if not item.ti_import then base else
 
     let xpath x = EcPath.pqname path x in
 
@@ -3003,15 +2978,15 @@ module Theory = struct
 
   (* ------------------------------------------------------------------ *)
   let bind
-    ?(import = import0)
-     (cth  : compiled_theory)
+    ?(import = true)
+     (cth : compiled_theory)
      (env : env)
   =
     let { cth_items = items; cth_mode = mode; } = cth.ctheory in
     let env = MC.bind_theory cth.name cth.ctheory env in
     let env = {
       env with
-        env_item = mkitem import (Th_theory (cth.name, cth.ctheory)) :: env.env_item }
+        env_item = mkitem ~import (Th_theory (cth.name, cth.ctheory)) :: env.env_item }
     in
 
     let env =
@@ -3047,21 +3022,17 @@ module Theory = struct
     let rec import (env : env) path (th : theory) =
       let xpath x = EcPath.pqname path x in
       let import_th_item (env : env) (item : theory_item) =
-        if not item.ti_import.im_atimport then env else
+        if not item.ti_import then env else
 
         match item.ti_item with
         | Th_type (x, ty) ->
-            if   ty.tyd_resolve
-            then MC.import_tydecl (xpath x) ty env
-            else env
+            MC.import_tydecl (xpath x) ty env
 
         | Th_operator (x, op) ->
             MC.import_operator (xpath x) op env
 
         | Th_axiom (x, ax) ->
-            if   ax.ax_visibility <> `Hidden
-            then MC.import_axiom (xpath x) ax env
-            else env
+            MC.import_axiom (xpath x) ax env
 
         | Th_modtype (x, mty) ->
             MC.import_modty (xpath x) mty env
@@ -3100,7 +3071,7 @@ module Theory = struct
   (* ------------------------------------------------------------------ *)
   let export (path : EcPath.path) lc (env : env) =
     let env = import path env in
-    { env with env_item = mkitem import0 (Th_export (path, lc)) :: env.env_item }
+    { env with env_item = mkitem ~import:true (Th_export (path, lc)) :: env.env_item }
 
   (* ------------------------------------------------------------------ *)
   let rec filter clears root cleared items =
diff --git a/src/ecEnv.mli b/src/ecEnv.mli
index 0ed659eb2..6b7955ce7 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -161,7 +161,7 @@ module Ax : sig
   val lookup_path : qsymbol -> env -> path
 
   val add  : path -> env -> env
-  val bind : ?import:import -> symbol -> t -> env -> env
+  val bind : ?import:bool -> symbol -> t -> env -> env
 
   val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit
   val all  : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list
@@ -184,7 +184,7 @@ module Mod : sig
   val sp_lookup     : qsymbol -> env -> spt
   val sp_lookup_opt : qsymbol -> env -> spt option
 
-  val bind  : ?import:import -> symbol -> t -> env -> env
+  val bind  : ?import:bool -> symbol -> t -> env -> env
   val enter : symbol -> (EcIdent.t * module_type) list -> env -> env
 
   val bind_local    : EcIdent.t -> mty_mr -> env -> env
@@ -215,7 +215,7 @@ module ModTy : sig
   val modtype : path -> env -> module_type
 
   val add  : path -> env -> env
-  val bind : ?import:import -> symbol -> t -> env -> env
+  val bind : ?import:bool -> symbol -> t -> env -> env
 
   val sig_of_mt : env -> module_type -> module_sig
 end
@@ -278,7 +278,7 @@ module Theory : sig
   val env_of_theory : path -> env -> env
 
   val add  : path -> env -> env
-  val bind : ?import:import -> compiled_theory -> env -> env
+  val bind : ?import:bool -> compiled_theory -> env -> env
 
  (* FIXME: section ? ctheory -> theory *)
   val require : compiled_theory -> env -> env
@@ -308,7 +308,7 @@ module Op : sig
   val lookup_path : qsymbol -> env -> path
 
   val add  : path -> env -> env
-  val bind : ?import:import -> symbol -> operator -> env -> env
+  val bind : ?import:bool -> symbol -> operator -> env -> env
 
   val reducible : ?mode:redmode -> ?nargs:int -> env -> path -> bool
   val reduce    : ?mode:redmode -> ?nargs:int -> env -> path -> ty list -> form
@@ -342,7 +342,7 @@ module Ty : sig
   val lookup_path : ?unique:bool -> qsymbol -> env -> path
 
   val add  : path -> env -> env
-  val bind : ?import:import -> symbol -> t -> env -> env
+  val bind : ?import:bool -> symbol -> t -> env -> env
 
   val defined : path -> env -> bool
   val unfold  : path -> EcTypes.ty list -> env -> EcTypes.ty
@@ -375,7 +375,7 @@ module TypeClass : sig
   type t = typeclass
 
   val add   : path -> env -> env
-  val bind  : ?import:import -> symbol -> t -> env -> env
+  val bind  : ?import:bool -> symbol -> t -> env -> env
   val graph : env -> EcTypeClass.graph
 
   val by_path     : path -> env -> t
@@ -384,7 +384,7 @@ module TypeClass : sig
   val lookup_opt  : qsymbol -> env -> (path * t) option
   val lookup_path : qsymbol -> env -> path
 
-  val add_instance  : ?import:import -> (ty_params * ty) -> tcinstance -> is_local -> env -> env
+  val add_instance  : ?import:bool -> (ty_params * ty) -> tcinstance -> is_local -> env -> env
   val get_instances : env -> ((ty_params * ty) * tcinstance) list
 end
 
@@ -396,8 +396,8 @@ module BaseRw : sig
   val lookup_path : qsymbol -> env -> path
   val is_base     : qsymbol -> env -> bool
 
-  val add   : ?import:import -> symbol -> is_local -> env -> env
-  val addto : ?import:import -> path -> path list -> is_local -> env -> env
+  val add   : ?import:bool -> symbol -> is_local -> env -> env
+  val addto : ?import:bool -> path -> path list -> is_local -> env -> env
 
   val all : env -> (path * Sp.t) list 
 end
@@ -409,7 +409,7 @@ module Reduction : sig
 
   val all : env -> (topsym * rule list) list
   val add1 : path * rule_option * rule option -> env -> env
-  val add  : ?import:import -> (path * rule_option * rule option) list -> env -> env
+  val add  : ?import:bool -> (path * rule_option * rule option) list -> env -> env
   val get  : topsym -> env -> rule list
 end
 
@@ -418,8 +418,8 @@ module Auto : sig
   type base0 = path * [`Rigid | `Default]
 
   val dname  : symbol
-  val add1   : ?import:import -> level:int -> ?base:symbol -> base0 -> is_local -> env -> env
-  val add    : ?import:import -> level:int -> ?base:symbol -> base0 list -> is_local -> env -> env
+  val add1   : ?import:bool -> level:int -> ?base:symbol -> base0 -> is_local -> env -> env
+  val add    : ?import:bool -> level:int -> ?base:symbol -> base0 list -> is_local -> env -> env
   val get    : ?base:symbol -> env -> base0 list
   val getall : symbol list -> env -> base0 list
   val getx   : symbol -> env -> (int * base0 list) list
diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml
index 16243fee3..a51dede08 100644
--- a/src/ecHiInductive.ml
+++ b/src/ecHiInductive.ml
@@ -86,7 +86,6 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
       tyd_params  = EcUnify.UniEnv.tparams ue;
       tyd_type    = `Abstract EcPath.Sp.empty;
       tyd_loca    = lc;
-      tyd_resolve = true;
     } in
       EcEnv.Ty.bind (unloc name) myself env
   in
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index 593a5abfc..efdad342a 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -2536,10 +2536,9 @@ let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) =
 
   let pp_decl fmt () =
     let vs =
-      match ax.ax_visibility with
-      | `Visible -> []
-      | `NoSmt   -> ["nosmt"]
-      | `Hidden  -> ["(* hidden *)"] in
+      match ax.ax_smt with
+      | true    -> []
+      | false   -> ["nosmt"] in
 
 
     Format.fprintf fmt "@[<hov 2>%a %t%t:@ %t.@]"
@@ -3445,8 +3444,8 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
     (pp_list "@,@," (pp_th_item ppe path)) cth.cth_items
     basename
 
- and pp_th_item ppe p fmt item =
-  match item.ti_item with
+ and pp_th_item_r ppe p fmt item =
+  match item.EcTheory.ti_item with
   | EcTheory.Th_type (id, ty) ->
       pp_typedecl ppe fmt (EcPath.pqname p id,ty)
 
@@ -3547,6 +3546,12 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
         level (odfl "" base)
         (pp_list "@ " (pp_axhnt ppe)) axioms
 
+(* -------------------------------------------------------------------- *)
+and pp_th_item ppe p fmt item =
+  Format.fprintf fmt "%s%a"
+    (if item.ti_import then "(* import *) " else "(* no import *) ")
+    (pp_th_item_r ppe p) item
+
 (* -------------------------------------------------------------------- *)
 let pp_stmt_with_nums (ppe : PPEnv.t) fmt stmt =
   let ppnode = collect2_s ppe stmt.s_node [] in
diff --git a/src/ecScope.ml b/src/ecScope.ml
index ac291529d..3d7818e2d 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -305,8 +305,8 @@ and proof_state =
   PSNoCheck | PSCheck of EcCoreGoal.proof
 
 and pucflags = {
-  puc_visibility : EcDecl.ax_visibility;
-  puc_local      : bool;
+  puc_smt   : bool;
+  puc_local : bool;
 }
 
 (* -------------------------------------------------------------------- *)
@@ -785,7 +785,7 @@ module Auto = struct
           hierror ~loc:base.pl_loc
             "cannot create rewrite hints out of its enclosing theory";
         let scope =
-          let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_baserw (ibase, local)) in
+          let item = EcTheory.mkitem ~import:true (EcTheory.Th_baserw (ibase, local)) in
           { scope with sc_env = EcSection.add_item item scope.sc_env; } in
         (scope, fst (EcEnv.BaseRw.lookup base.pl_desc (env scope)))
 
@@ -793,11 +793,11 @@ module Auto = struct
 
     let env = env scope in
     let l = List.map (fun l -> EcEnv.Ax.lookup_path (unloc l) env) l in
-    let item = EcTheory.mkitem EcTheory.import0 (Th_addrw (base, l, local)) in
+    let item = EcTheory.mkitem ~import:true (Th_addrw (base, l, local)) in
     { scope with sc_env =  EcSection.add_item item scope.sc_env }
 
   let bind_hint scope ~local ~level ?base axioms =
-    let item = EcTheory.mkitem EcTheory.import0 (Th_auto { level; base; axioms; locality=local} ) in
+    let item = EcTheory.mkitem ~import:true (Th_auto { level; base; axioms; locality=local} ) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   let add_hint scope hint =
@@ -822,9 +822,9 @@ module Ax = struct
   type proofmode = Tactics.proofmode
 
   (* ------------------------------------------------------------------ *)
-  let bind ?(import = EcTheory.import0) (scope : scope) ((x, ax) : _ * axiom) =
+  let bind ?(import = true) (scope : scope) ((x, ax) : _ * axiom) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_axiom (x, ax)) in
+    let item = EcTheory.mkitem ~import (EcTheory.Th_axiom (x, ax)) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
@@ -890,11 +890,11 @@ module Ax = struct
         | PAxiom tags -> `Axiom (Ssym.of_list (List.map unloc tags), false)
         | _ -> `Lemma
 
-      in { ax_tparams    = tparams;
-           ax_spec       = concl;
-           ax_kind       = kind;
-           ax_loca       = ax.pa_locality;
-           ax_visibility = `Visible; }
+      in { ax_tparams = tparams;
+           ax_spec    = concl;
+           ax_kind    = kind;
+           ax_loca    = ax.pa_locality;
+           ax_smt     = true; }
     in
 
     match ax.pa_kind with
@@ -906,7 +906,7 @@ module Ax = struct
           | `Global  -> false in
 
         let check    = Check_mode.check scope.sc_options in
-        let pucflags = { puc_visibility = axd.ax_visibility; puc_local = local; } in
+        let pucflags = { puc_smt = axd.ax_smt; puc_local = local; } in
         let pucflags = (([], None), pucflags) in
 
         match tc with
@@ -1060,7 +1060,7 @@ module Ax = struct
       in
         doit [] (fst puc.puc_cont)
     in
-    let pucflags = { puc_visibility = ax.ax_visibility; puc_local = false; } in
+    let pucflags = { puc_smt = ax.ax_smt; puc_local = false; } in
     let pucflags = ((proofs, snd puc.puc_cont), pucflags) in
     let check    = Check_mode.check scope.sc_options in
 
@@ -1085,9 +1085,9 @@ module Op = struct
   module TT  = EcTyping
   module EHI = EcHiInductive
 
-  let bind ?(import = EcTheory.import0) (scope : scope) ((x, op) : _ * operator) =
+  let bind ?(import = true) (scope : scope) ((x, op) : _ * operator) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_operator (x, op)) in
+    let item = EcTheory.mkitem ~import (EcTheory.Th_operator (x, op)) in
     { scope with sc_env = EcSection.add_item item scope.sc_env; }
 
   let add (scope : scope) (op : poperator located) =
@@ -1220,11 +1220,11 @@ module Op = struct
               (Tvar.f_subst ~freshen:true bdpm (List.map EcTypes.tvar axpm) ax,
                List.combine axpm (List.map snd tparams)) in
           let ax =
-            { ax_tparams    = axpm;
-              ax_spec       = ax;
-              ax_kind       = `Axiom (Ssym.empty, false);
-              ax_loca       = lc;
-              ax_visibility = `Visible; }
+            { ax_tparams = axpm;
+              ax_spec    = ax;
+              ax_kind    = `Axiom (Ssym.empty, false);
+              ax_loca    = lc;
+              ax_smt     = true; }
           in Ax.bind scope (unloc rname, ax))
         scope refts
     in
@@ -1273,11 +1273,11 @@ module Op = struct
       let ax  = EcFol.f_forall (List.map (snd_map gtty) bds) ax in
 
       let ax =
-        { ax_tparams    = List.map (fun ty -> (ty, Sp.empty)) nparams;
-          ax_spec       = ax;
-          ax_kind       = `Axiom (Ssym.empty, false);
-          ax_loca       = lc;
-          ax_visibility = `Visible; } in
+        { ax_tparams = List.map (fun ty -> (ty, Sp.empty)) nparams;
+          ax_spec    = ax;
+          ax_kind    = `Axiom (Ssym.empty, false);
+          ax_loca    = lc;
+          ax_smt     = true; } in
 
       let scope, axname =
         let axname = Printf.sprintf "%s_%s" (unloc op.po_name) suffix in
@@ -1398,11 +1398,11 @@ module Op = struct
       in
 
       let prax = EcDecl.{
-        ax_tparams    = [];
-        ax_spec       = prax;
-        ax_kind       = `Lemma;
-        ax_loca       = op.ppo_locality;
-        ax_visibility = `Visible;
+        ax_tparams = [];
+        ax_spec    = prax;
+        ax_kind    = `Lemma;
+        ax_loca    = op.ppo_locality;
+        ax_smt     = true;
       } in
 
       Ax.bind scope (unloc op.ppo_name ^ "_opsem", prax) in
@@ -1431,11 +1431,11 @@ module Op = struct
          in
 
          let prax = EcDecl.{
-           ax_tparams    = [];
-           ax_spec       = hax;
-           ax_kind       = `Lemma;
-           ax_loca       = op.ppo_locality;
-           ax_visibility = `Visible;
+           ax_tparams = [];
+           ax_spec    = hax;
+           ax_kind    = `Lemma;
+           ax_loca    = op.ppo_locality;
+           ax_smt     = true;
          } in
 
          Ax.bind scope (unloc op.ppo_name ^ "_opsem_det", prax)
@@ -1475,9 +1475,9 @@ end
 module Mod = struct
   module TT = EcTyping
 
-  let bind ?(import = EcTheory.import0) (scope : scope) (m : top_module_expr) =
+  let bind ?(import = true) (scope : scope) (m : top_module_expr) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_module m) in
+    let item = EcTheory.mkitem ~import (EcTheory.Th_module m) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   let add_concrete (scope : scope) lc (ptm : pmodule_def) =
@@ -1534,11 +1534,11 @@ end
 (* -------------------------------------------------------------------- *)
 module ModType = struct
   let bind
-        ?(import = EcTheory.import0) (scope : scope)
+        ?(import = true) (scope : scope)
         ((x, tysig) : _ * top_module_sig)
   =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_modtype (x, tysig)) in
+    let item = EcTheory.mkitem ~import (EcTheory.Th_modtype (x, tysig)) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   let add (scope : scope) (intf : pinterface) =
@@ -1565,9 +1565,9 @@ module Ty = struct
       hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc
 
   (* ------------------------------------------------------------------ *)
-  let bind ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) =
+  let bind ?(import = true) (scope : scope) ((x, tydecl) : (_ * tydecl)) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_type (x, tydecl)) in
+    let item = EcTheory.mkitem ~import (EcTheory.Th_type (x, tydecl)) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
@@ -1608,12 +1608,12 @@ module Ty = struct
         record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
     in
 
-    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; })
+    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; })
 
   (* ------------------------------------------------------------------ *)
-  let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) =
+  let bindclass ?(import = true) (scope : scope) (x, tc) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_typeclass(x, tc)) in
+    let item = EcTheory.mkitem ~import (EcTheory.Th_typeclass(x, tc)) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
@@ -1639,8 +1639,7 @@ module Ty = struct
         let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
           { tyd_params  = [];
             tyd_type    = `Abstract body;
-            tyd_loca    = (lc :> locality);
-            tyd_resolve = true;  } in
+            tyd_loca    = (lc :> locality); } in
       let scenv = EcEnv.Ty.bind name asty scenv in
 
       (* Check for duplicated field names *)
@@ -1755,11 +1754,11 @@ module Ty = struct
         (fun (x, req) ->
            if not (Mstr.mem x symbs) then
              let ax = {
-               ax_tparams    = [];
-               ax_spec       = req;
-               ax_kind       = `Lemma;
-               ax_loca       = lc;
-               ax_visibility = `NoSmt;
+               ax_tparams = [];
+               ax_spec    = req;
+               ax_kind    = `Lemma;
+               ax_loca    = lc;
+               ax_smt     = false;
              } in Some ((None, ax), EcPath.psymbol x, scope.sc_env)
            else None)
         reqs in
@@ -1770,14 +1769,14 @@ module Ty = struct
           let t  = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in
           let t  = { pt_core = t; pt_intros = []; } in
           let ax = {
-              ax_tparams    = [];
-              ax_spec       = f;
-              ax_kind       = `Lemma;
-              ax_visibility = `NoSmt;
-              ax_loca       = lc;
+              ax_tparams = [];
+              ax_spec    = f;
+              ax_kind    = `Lemma;
+              ax_smt     = false;
+              ax_loca    = lc;
           } in
 
-          let pucflags = { puc_visibility = `Visible; puc_local = false; } in
+          let pucflags = { puc_smt = true; puc_local = false; } in
           let pucflags = (([], None), pucflags) in
           let check    = Check_mode.check scope.sc_options in
 
@@ -1836,7 +1835,7 @@ module Ty = struct
     let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc in
     let add env p =
       let item = EcTheory.Th_instance (ty,`General p, tci.pti_loca) in
-      let item = EcTheory.mkitem import item in
+      let item = EcTheory.mkitem ~import item in
       EcSection.add_item item env in
 
     let scope   =
@@ -1844,7 +1843,7 @@ module Ty = struct
           List.fold_left add
             (let item =
                EcTheory.Th_instance (([], snd ty), `Ring cr, tci.pti_loca) in
-             let item = EcTheory.mkitem import item in
+             let item = EcTheory.mkitem ~import item in
              EcSection.add_item item scope.sc_env)
             [p_zmod; p_ring; p_idomain] }
 
@@ -1878,7 +1877,7 @@ module Ty = struct
     let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc; in
     let add env p =
       let item = EcTheory.Th_instance(ty,`General p, tci.pti_loca) in
-      let item = EcTheory.mkitem import item in
+      let item = EcTheory.mkitem ~import item in
       EcSection.add_item item env in
     let scope   =
       { scope with
@@ -1886,7 +1885,7 @@ module Ty = struct
           List.fold_left add
             (let item =
                EcTheory.Th_instance (([], snd ty), `Field cr, tci.pti_loca) in
-             let item = EcTheory.mkitem import item in
+             let item = EcTheory.mkitem ~import item in
               EcSection.add_item item scope.sc_env)
             [p_zmod; p_ring; p_idomain; p_field] }
 
@@ -1933,14 +1932,12 @@ module Ty = struct
 *)
 
   (* ------------------------------------------------------------------ *)
-  let add_instance
-    ?(import = EcTheory.import0) (scope : scope) mode ({ pl_desc = tci } as toptci)
-  =
+  let add_instance (scope : scope) mode ({ pl_desc = tci } as toptci) =
     match unloc tci.pti_name with
     | ([], "bring") -> begin
         if EcUtils.is_some tci.pti_args then
           hierror "unsupported-option";
-        addring ~import scope mode (`Boolean, toptci)
+        addring ~import:true scope mode (`Boolean, toptci)
     end
 
     | ([], "ring") -> begin
@@ -1956,10 +1953,10 @@ module Ty = struct
                  && opt_equal BI.equal p (Some (BI.of_int 2))
             then `Boolean
             else `Modulus (c, p)
-      in addring ~import scope mode (kind, toptci)
+      in addring ~import:true scope mode (kind, toptci)
     end
 
-    | ([], "field") -> addfield ~import scope mode toptci
+    | ([], "field") -> addfield ~import:true scope mode toptci
 
     | _ ->
         if EcUtils.is_some tci.pti_args then
@@ -1974,10 +1971,10 @@ module Theory = struct
   exception TopScope
 
   (* ------------------------------------------------------------------ *)
-  let bind (scope : scope) (cth : thloaded) =
+  let bind ?(import = true) (scope : scope) (cth : thloaded) =
     assert (scope.sc_pr_uc = None);
     { scope with
-        sc_env = EcSection.add_th ~import:EcTheory.import0 cth scope.sc_env }
+        sc_env = EcSection.add_th ~import cth scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
   let required (scope : scope) (name : required_info) =
@@ -2055,13 +2052,13 @@ module Theory = struct
       ((cth, required), scope.sc_name, sup)
 
   (* ------------------------------------------------------------------ *)
-  let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
+  let exit ?import ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
     assert (scope.sc_pr_uc = None);
 
     let cth = exit_r ~pempty (add_clears clears scope) in
     let ((cth, required), (name, _), scope) = cth in
     let scope = List.fold_right require_loaded required scope in
-    let scope = ofold (fun cth scope -> bind scope cth) scope cth in
+    let scope = ofold (fun cth scope -> bind ?import scope cth) scope cth in
     (name, scope)
 
   (* ------------------------------------------------------------------ *)
@@ -2092,7 +2089,7 @@ module Theory = struct
 
   (* ------------------------------------------------------------------ *)
   let export_p scope (p, lc) =
-    let item = mkitem EcTheory.import0 (EcTheory.Th_export (p, lc)) in
+    let item = mkitem ~import:true (EcTheory.Th_export (p, lc)) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   let export (scope : scope) (name : qsymbol) =
@@ -2197,7 +2194,7 @@ module Reduction = struct
 
     in
 
-    let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_reduction rules) in
+    let item = EcTheory.mkitem ~import:true (EcTheory.Th_reduction rules) in
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 end
 
@@ -2212,9 +2209,10 @@ module Cloning = struct
 
   (* ------------------------------------------------------------------ *)
   let hooks : scope R.ovrhooks =
-    let thexit sc pempty = snd (Theory.exit ?clears:None ~pempty sc) in
-    let add_item scope import item =
-      let item = EcTheory.mkitem import item in
+    let thexit sc ~import pempty =
+      snd (Theory.exit ~import ?clears:None ~pempty sc) in
+    let add_item scope ~import item =
+      let item = EcTheory.mkitem ~import item in
       { scope with sc_env = EcSection.add_item item scope.sc_env } in
     { R.henv      = (fun scope -> scope.sc_env);
       R.hadd_item = add_item;
@@ -2263,7 +2261,7 @@ module Cloning = struct
       EcTheoryReplay.replay hooks
         ~abstract:opts.R.clo_abstract ~local:thcl.pthc_local ~incl
         ~clears:ntclr ~renames:rnms ~opath ~npath ovrds
-        scope (name, oth.cth_items)
+        scope (name, false, oth.cth_items)
     in
 
     let proofs = List.pmap (fun axc ->
@@ -2277,7 +2275,7 @@ module Cloning = struct
           let t = { pt_core = t; pt_intros = []; } in
           let (x, ax) = axc.C.axc_axiom in
 
-          let pucflags = { puc_visibility = `Visible; puc_local = false; } in
+          let pucflags = { puc_smt = true; puc_local = false; } in
           let pucflags = (([], None), pucflags) in
           let check    = Check_mode.check scope.sc_options in
 
@@ -2295,7 +2293,7 @@ module Cloning = struct
         | `Import  ->
           { scope with sc_env = EcSection.import npath scope.sc_env; }
         | `Export  ->
-          let item = EcTheory.mkitem EcTheory.import0 (Th_export (npath, `Global)) in
+          let item = EcTheory.mkitem ~import:true (Th_export (npath, `Global)) in
           { scope with sc_env = EcSection.add_item item scope.sc_env; }
         | `Include -> scope)
         scope
diff --git a/src/ecScope.mli b/src/ecScope.mli
index f04f9595a..5a06627d8 100644
--- a/src/ecScope.mli
+++ b/src/ecScope.mli
@@ -50,8 +50,8 @@ and proof_state =
   PSNoCheck | PSCheck of EcCoreGoal.proof
 
 and pucflags = {
-  puc_visibility : EcDecl.ax_visibility;
-  puc_local      : bool;
+  puc_smt   : bool;
+  puc_local : bool;
 }
 
 (* -------------------------------------------------------------------- *)
@@ -119,7 +119,7 @@ module Ty : sig
   val add : scope -> ptydecl located -> scope
 
   val add_class    : scope -> ptypeclass located -> scope
-  val add_instance : ?import:EcTheory.import -> scope -> Ax.proofmode -> ptycinstance located -> scope
+  val add_instance : scope -> Ax.proofmode -> ptycinstance located -> scope
 end
 
 (* -------------------------------------------------------------------- *)
@@ -151,7 +151,8 @@ module Theory : sig
   (* [exit scope] close and finalize the top-most theory and returns
    * its name. Raises [TopScope] if [scope] has not super scope. *)
   val exit :
-       ?pempty:[`ClearOnly | `Full | `No]
+       ?import:bool
+    -> ?pempty:[`ClearOnly | `Full | `No]
     -> ?clears:(pqsymbol option) list
     -> scope -> symbol * scope
 
diff --git a/src/ecSection.ml b/src/ecSection.ml
index 3c8257547..9748fa130 100644
--- a/src/ecSection.ml
+++ b/src/ecSection.ml
@@ -786,8 +786,7 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
     let to_gen = { to_gen with tg_subst} in
     let tydecl = {
         tyd_params; tyd_type;
-        tyd_loca = `Global;
-        tyd_resolve = tydecl.tyd_resolve } in
+        tyd_loca = `Global; } in
     to_gen, Some (Th_type (name, tydecl))
 
   | `Declare ->
@@ -1339,22 +1338,24 @@ let exit_theory ?clears ?pempty scenv =
 let add_item_ (item : theory_item) (scenv:scenv) =
   let item = if scenv.sc_loca = `Local then set_local_item item else item in
   let env = scenv.sc_env in
+  let import = item.ti_import in
   let env =
     match item.ti_item with
-    | Th_type    (s,tyd)     -> EcEnv.Ty.bind s tyd env
-    | Th_operator (s,op)     -> EcEnv.Op.bind s op env
-    | Th_axiom   (s, ax)     -> EcEnv.Ax.bind s ax env
-    | Th_modtype (s, ms)     -> EcEnv.ModTy.bind s ms env
-    | Th_module       me     -> EcEnv.Mod.bind me.tme_expr.me_name me env
-    | Th_typeclass(s,tc)     -> EcEnv.TypeClass.bind s tc env
-    | Th_export  (p, lc)     -> EcEnv.Theory.export p lc env
-    | Th_instance (tys,i,lc) -> EcEnv.TypeClass.add_instance tys i lc env
-    | Th_baserw   (s,lc)     -> EcEnv.BaseRw.add s lc env
-    | Th_addrw (p,ps,lc)     -> EcEnv.BaseRw.addto p ps lc env
-    | Th_auto auto           -> EcEnv.Auto.add ~level:auto.level ?base:auto.base
-                                  auto.axioms auto.locality env
-    | Th_reduction r         -> EcEnv.Reduction.add r env
-    | _                      -> assert false
+    | Th_type    (s,tyd) -> EcEnv.Ty.bind ~import s tyd env
+    | Th_operator (s,op) -> EcEnv.Op.bind ~import s op env
+    | Th_axiom   (s, ax) -> EcEnv.Ax.bind ~import s ax env
+    | Th_modtype (s, ms) -> EcEnv.ModTy.bind ~import s ms env
+    | Th_module       me -> EcEnv.Mod.bind ~import me.tme_expr.me_name me env
+    | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind ~import s tc env
+    | Th_export  (p, lc) -> EcEnv.Theory.export p lc env
+    | Th_instance (tys,i,lc) -> EcEnv.TypeClass.add_instance ~import tys i lc env (*FIXME: import? *)
+    | Th_baserw   (s,lc) -> EcEnv.BaseRw.add ~import s lc env
+    | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto ~import p ps lc env
+    | Th_auto auto       -> EcEnv.Auto.add
+                              ~import ~level:auto.level ?base:auto.base
+                              auto.axioms auto.locality env
+    | Th_reduction r     -> EcEnv.Reduction.add ~import r env
+    | _                  -> assert false
   in
   { scenv with
     sc_env = env;
@@ -1430,7 +1431,7 @@ and generalize_ctheory
     | Some compiled when List.is_empty compiled.ctheory.cth_items ->
       genenv
     | Some compiled ->
-      let scenv = add_th ~import:import0 compiled genenv.tg_env in
+      let scenv = add_th ~import:true compiled genenv.tg_env in
       { genenv with tg_env = scenv; }
 
 and generalize_lc_item (genenv : to_gen) (prefix : path) (item : sc_item) =
diff --git a/src/ecSection.mli b/src/ecSection.mli
index 5eb77909d..cbe163bfd 100644
--- a/src/ecSection.mli
+++ b/src/ecSection.mli
@@ -30,7 +30,7 @@ val import : EcPath.path -> scenv -> scenv
 
 val import_vars : EcPath.mpath -> scenv -> scenv
 
-val add_th  : import:import -> EcEnv.Theory.compiled_theory -> scenv -> scenv
+val add_th  : import:bool -> EcEnv.Theory.compiled_theory -> scenv -> scenv
 val require : EcEnv.Theory.compiled_theory -> scenv -> scenv
 
 val astop : scenv -> scenv
diff --git a/src/ecSmt.ml b/src/ecSmt.ml
index 6d81016c6..032d9e002 100644
--- a/src/ecSmt.ml
+++ b/src/ecSmt.ml
@@ -1540,7 +1540,7 @@ let init_relevant env pi rs =
   let push e r = r := e :: !r in
   let do1 p ax =
     let wanted = wanted_ax p in
-    if wanted || (ax.ax_visibility = `Visible && not (unwanted_ax p)) then begin
+    if wanted || (ax.ax_smt && not (unwanted_ax p)) then begin
       Frequency.add fr ax.ax_spec;
       let used = Frequency.f_ops unwanted_ops ax.ax_spec in
       let paxu = (p,ax), used in
@@ -1631,7 +1631,7 @@ let init hyps concl =
 let select env pi hyps concl execute_task =
   if pi.P.pr_all then
     let init_select p ax =
-      ax.ax_visibility = `Visible && not (P.Hints.mem p pi.P.pr_unwanted) in
+      ax.ax_smt && not (P.Hints.mem p pi.P.pr_unwanted) in
     (execute_task (EcEnv.Ax.all ~check:init_select env) = Some true)
   else
     let rs = Frequency.f_ops_goal unwanted_ops hyps.h_local concl in
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index d1b24f4f6..d57db7077 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -883,7 +883,6 @@ let subst_tydecl (s : subst) (tyd : tydecl) =
 
   { tyd_params  = tparams;
     tyd_type    = body;
-    tyd_resolve = tyd.tyd_resolve;
     tyd_loca    = tyd.tyd_loca; }
 
 (* -------------------------------------------------------------------- *)
@@ -976,11 +975,11 @@ let subst_ax (s : subst) (ax : axiom) =
   let s, tparams = fresh_tparams s ax.ax_tparams in
   let spec   = subst_form s ax.ax_spec in
 
-  { ax_tparams    = tparams;
-    ax_spec       = spec;
-    ax_kind       = ax.ax_kind;
-    ax_loca       = ax.ax_loca;
-    ax_visibility = ax.ax_visibility; }
+  { ax_tparams = tparams;
+    ax_spec    = spec;
+    ax_kind    = ax.ax_kind;
+    ax_loca    = ax.ax_loca;
+    ax_smt     = ax.ax_smt; }
 
 (* -------------------------------------------------------------------- *)
 let fresh_scparam (s : subst) ((x, ty) : EcIdent.t * ty) =
diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml
index 5ed2df1d2..46e1e7814 100644
--- a/src/ecThCloning.ml
+++ b/src/ecThCloning.ml
@@ -62,7 +62,7 @@ type evclone = {
   evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
-  evc_ths      : evclone Msym.t;
+  evc_ths      : (evclone * bool) Msym.t;
 }
 
 and evlemma = {
@@ -91,7 +91,9 @@ let rec evc_update (upt : evclone -> evclone) (nm : symbol list) (evc : evclone)
   | x :: nm ->
       let ths =
         Msym.change
-          (fun sub -> Some (evc_update upt nm (odfl evc_empty sub)))
+          (fun sub ->
+            let subevc, clear = odfl (evc_empty, false) sub in
+            Some (evc_update upt nm subevc, clear))
           x evc.evc_ths
       in
         { evc with evc_ths = ths }
@@ -101,8 +103,8 @@ let rec evc_get (nm : symbol list) (evc : evclone) =
   | []      -> Some evc
   | x :: nm ->
       match Msym.find_opt x evc.evc_ths with
-      | None     -> None
-      | Some evc -> evc_get nm evc
+      | None -> None
+      | Some (evc, _) -> evc_get nm evc
 
 (* -------------------------------------------------------------------- *)
 let find_mc =
@@ -390,6 +392,13 @@ end = struct
     let thd  = let thd = EcPath.toqsymbol sp in (fst thd @ [snd thd]) in
     let xdth = nm @ [x] in
 
+    assert (not (Msym.mem x evc.evc_ths));
+
+    let evc = { evc with
+      evc_ths = Msym.change (fun sub ->
+        let sub, clear = odfl (evc_empty, false) sub in
+        Some (sub, clear || (mode <> `Alias))) x evc.evc_ths } in
+
     let rec doit_r prefix (proofs, evc) dth =
       match dth with
       | Th_type (x, _) ->
diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli
index b4206554d..cd303fc10 100644
--- a/src/ecThCloning.mli
+++ b/src/ecThCloning.mli
@@ -48,7 +48,7 @@ type evclone = {
   evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
-  evc_ths      : evclone Msym.t;
+  evc_ths      : (evclone * bool) Msym.t;
 }
 
 and evlemma = {
diff --git a/src/ecTheory.ml b/src/ecTheory.ml
index a329d9318..76de53424 100644
--- a/src/ecTheory.ml
+++ b/src/ecTheory.ml
@@ -10,18 +10,12 @@ open EcModules
 (* -------------------------------------------------------------------- *)
 module Sp = EcPath.Sp
 
-(* -------------------------------------------------------------------- *)
-type import = { im_immediate : bool; im_atimport : bool; }
-
-let import0  = { im_immediate =  true; im_atimport =  true; }
-let noimport = { im_immediate = false; im_atimport = false; }
-
 (* -------------------------------------------------------------------- *)
 type theory = theory_item list
 
 and theory_item = {
   ti_item   : theory_item_r;
-  ti_import : import;
+  ti_import : bool;
 }
 
 and theory_item_r =
@@ -82,7 +76,7 @@ and auto_rule = {
   locality : is_local;
 }
 
-let mkitem (import : import) (item : theory_item_r) =
+let mkitem ~(import : bool) (item : theory_item_r) =
   { ti_import = import; ti_item = item; }
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecTheory.mli b/src/ecTheory.mli
index fb63e8544..1717eb778 100644
--- a/src/ecTheory.mli
+++ b/src/ecTheory.mli
@@ -6,18 +6,12 @@ open EcTypes
 open EcDecl
 open EcModules
 
-(* -------------------------------------------------------------------- *)
-type import = { im_immediate : bool; im_atimport : bool; }
-
-val import0  : import
-val noimport : import
-
 (* -------------------------------------------------------------------- *)
 type theory = theory_item list
 
 and theory_item = {
   ti_item   : theory_item_r;
-  ti_import : import;
+  ti_import : bool;
 }
 
 and theory_item_r =
@@ -79,7 +73,7 @@ and auto_rule = {
   locality : is_local;
 }
 
-val mkitem : import -> theory_item_r -> theory_item
+val mkitem : import:bool -> theory_item_r -> theory_item
 
 (* -------------------------------------------------------------------- *)
 val module_expr_of_module_sig : EcIdent.t -> mty_mr -> module_sig -> module_expr
diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 0b122511b..b7d34b23c 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -34,9 +34,9 @@ type 'a ovrenv = {
 
 and 'a ovrhooks = {
   henv      : 'a -> EcSection.scenv;
-  hadd_item : 'a -> EcTheory.import -> EcTheory.theory_item_r -> 'a;
+  hadd_item : 'a -> import:bool -> EcTheory.theory_item_r -> 'a;
   hthenter  : 'a -> thmode -> symbol -> is_local -> 'a;
-  hthexit   : 'a -> [`Full | `ClearOnly | `No] -> 'a;
+  hthexit   : 'a -> import:bool -> [`Full | `ClearOnly | `No] -> 'a;
   herr      : 'b . ?loc:EcLocation.t -> string -> 'b;
 }
 
@@ -323,7 +323,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
       let otyd = EcSubst.subst_tydecl subst otyd in
       let subst, x = rename ove subst (`Type, x) in
       let item = (Th_type (x, otyd)) in
-      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import item)
+      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import item)
 
   | Some { pl_desc = (tydov, mode) } -> begin
       let newtyd, body =
@@ -337,7 +337,6 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
             let decl  =
               { tyd_params  = nargs;
                 tyd_type    = `Concrete ntyd;
-                tyd_resolve = otyd.tyd_resolve && (mode = `Alias);
                 tyd_loca    = otyd.tyd_loca; }
 
             in (decl, ntyd)
@@ -347,10 +346,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
             | Some reftyd ->
                 let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) reftyd.tyd_params in
                 let body   = tconstr p tyargs in
-                let decl   =
-                  { reftyd with
-                      tyd_type    = `Concrete body;
-                      tyd_resolve = otyd.tyd_resolve && (mode = `Alias); } in
+                let decl   = { reftyd with tyd_type = `Concrete body; } in
                 (decl, body)
 
             | _ -> assert false
@@ -403,11 +399,11 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
         match mode with
         | `Alias ->
             let item = EcTheory.Th_type (x, newtyd) in
-            ove.ovre_hooks.hadd_item scope import item
+            ove.ovre_hooks.hadd_item scope ~import item
 
         | `Inline `Keep ->
             let item = EcTheory.Th_type (x, newtyd) in
-            ove.ovre_hooks.hadd_item scope EcTheory.noimport item
+            ove.ovre_hooks.hadd_item scope ~import:false item
 
         | `Inline `Clear ->
             scope
@@ -424,7 +420,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
   | None ->
       let (subst, x) = rename ove subst (`Op, x) in
       let oopd = EcSubst.subst_op subst oopd in
-      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import (Th_operator (x, oopd)))
+      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import (Th_operator (x, oopd)))
 
   | Some { pl_desc = (opov, opmode); pl_loc = loc; } ->
       let refop = EcSubst.subst_op subst oopd in
@@ -516,11 +512,11 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
         match opmode with
         | `Alias ->
             let item = Th_operator (x, newop) in
-            ove.ovre_hooks.hadd_item scope import item
+            ove.ovre_hooks.hadd_item scope ~import item
 
         | `Inline `Keep ->
             let item = Th_operator (x, newop) in
-            ove.ovre_hooks.hadd_item scope EcTheory.noimport item
+            ove.ovre_hooks.hadd_item scope ~import:false item
 
         | `Inline `Clear ->
             scope
@@ -535,7 +531,7 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) =
   | None ->
       let subst, x = rename ove subst (`Pred, x) in
       let oopr = EcSubst.subst_op subst oopr in
-      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import (Th_operator (x, oopr)))
+      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import (Th_operator (x, oopr)))
 
   | Some { pl_desc = (prov, prmode); pl_loc = loc; } ->
     let refpr = EcSubst.subst_op subst oopr in
@@ -626,11 +622,11 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) =
       match prmode with
       | `Alias ->
           let item = Th_operator (x, newpr) in
-          ove.ovre_hooks.hadd_item scope import item
+          ove.ovre_hooks.hadd_item scope ~import item
 
       | `Inline `Keep ->
           let item = Th_operator (x, newpr) in
-          ove.ovre_hooks.hadd_item scope EcTheory.noimport item
+          ove.ovre_hooks.hadd_item scope ~import:false item
 
       | `Inline `Clear ->
           scope
@@ -647,7 +643,7 @@ and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oont) =
       let subst, x = rename ove subst (`Op, x) in
       let oont = EcSubst.subst_op subst oont in
       let item = Th_operator (x, oont) in
-      let scope = ove.ovre_hooks.hadd_item scope import item in
+      let scope = ove.ovre_hooks.hadd_item scope ~import item in
       (subst, ops, proofs, scope)
 
   | Some { pl_desc = (_, mode) } -> begin
@@ -656,7 +652,7 @@ and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oont) =
       let subst, x = rename ove subst (`Op, x) in
       let oont = EcSubst.subst_op subst oont in
       let item = Th_operator (x, oont) in
-      let scope = ove.ovre_hooks.hadd_item scope import item in
+      let scope = ove.ovre_hooks.hadd_item scope ~import item in
       (subst, ops, proofs, scope)
     | `Inline `Clear ->
       (subst, ops, proofs, scope)
@@ -692,10 +688,7 @@ and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
       | Some (pt, hide, explicit)  ->
           if explicit && not (EcDecl.is_axiom ax.ax_kind) then
             clone_error (EcSection.env scenv) (CE_ProofForLemma (snd ove.ovre_prefix, x));
-          let ax  = { ax with
-            ax_kind = `Lemma;
-            ax_visibility = if hide <> `Alias then `Hidden else ax.ax_visibility
-          } in
+          let ax  = { ax with ax_kind = `Lemma } in
           let axc = { axc_axiom = (x, ax);
                       axc_path  = EcPath.fromqsymbol (snd ove.ovre_prefix, x);
                       axc_tac   = pt;
@@ -704,7 +697,7 @@ and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
 
   let scope =
     if axclear then scope else
-      ove.ovre_hooks.hadd_item scope import (Th_axiom(x, ax))
+      ove.ovre_hooks.hadd_item scope ~import (Th_axiom(x, ax))
   in (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -716,7 +709,7 @@ and replay_modtype
       let subst, x = rename ove subst (`ModType, x) in
       let modty = EcSubst.subst_top_modsig subst modty in
       let item = Th_modtype (x, modty) in
-      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import item)
+      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import item)
 
   | Some { pl_desc = (newname, mode) } ->
       let env = EcSection.env (ove.ovre_hooks.henv scope) in
@@ -736,7 +729,7 @@ and replay_modtype
       let scope =
         if keep_of_mode mode then
           let item = Th_modtype (name, newmt) in
-          ove.ovre_hooks.hadd_item scope import item
+          ove.ovre_hooks.hadd_item scope ~import item
         else scope
       in (subst, ops, proofs, scope)
 
@@ -750,7 +743,7 @@ and replay_mod
       let me = EcSubst.subst_top_module subst me in
       let me = { me with tme_expr = { me.tme_expr with me_name = name } } in
       let item = (Th_module me) in
-      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import item)
+      (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import item)
 
   | Some { pl_desc = (newname, mode) } ->
       let name  = me.tme_expr.me_name in
@@ -788,7 +781,7 @@ and replay_mod
 
       let scope =
         if   keep_of_mode mode
-        then ove.ovre_hooks.hadd_item scope import (Th_module newme)
+        then ove.ovre_hooks.hadd_item scope ~import (Th_module newme)
         else scope in
 
       (subst, ops, proofs, scope)
@@ -804,14 +797,14 @@ and replay_export
   if is_none (EcEnv.Theory.by_path_opt p env) then
     (subst, ops, proofs, scope)
   else
-    let scope = ove.ovre_hooks.hadd_item scope import (Th_export (p, lc)) in
+    let scope = ove.ovre_hooks.hadd_item scope ~import (Th_export (p, lc)) in
     (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
 and replay_baserw
   (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, lc)
 =
-  let scope = ove.ovre_hooks.hadd_item scope import (Th_baserw (name, lc)) in
+  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_baserw (name, lc)) in
   (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -820,7 +813,7 @@ and replay_addrw
 =
   let p     = EcSubst.subst_path subst p in
   let l     = List.map (EcSubst.subst_path subst) l in
-  let scope = ove.ovre_hooks.hadd_item scope import (Th_addrw (p, l, lc)) in
+  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_addrw (p, l, lc)) in
   (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -830,7 +823,7 @@ and replay_auto
   let env = EcSection.env (ove.ovre_hooks.henv scope) in
   let axioms = List.map (fst_map (EcSubst.subst_path subst)) at_base.axioms in
   let axioms = List.filter (fun (p, _) -> Option.is_some (EcEnv.Ax.by_path_opt p env)) axioms in
-  let scope = ove.ovre_hooks.hadd_item scope import (Th_auto { at_base with axioms }) in
+  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_auto { at_base with axioms }) in
   (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -856,7 +849,7 @@ 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 scope = ove.ovre_hooks.hadd_item scope ~import (Th_reduction rules) in
 
   (subst, ops, proofs, scope)
 
@@ -865,7 +858,7 @@ and replay_typeclass
   (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, tc)
 =
   let tc = EcSubst.subst_tc subst tc in
-  let scope = ove.ovre_hooks.hadd_item scope import (Th_typeclass (x, tc)) in
+  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_typeclass (x, tc)) in
   (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -939,62 +932,66 @@ and replay_instance
         | `General p  -> `General (forpath p)
     in
 
-    let scope = ove.ovre_hooks.hadd_item scope import (Th_instance ((typ, ty), tc, lc)) in
+    let scope = ove.ovre_hooks.hadd_item scope ~import (Th_instance ((typ, ty), tc, lc)) in
     (subst, ops, proofs, scope)
 
   with E.InvInstPath ->
     (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
-and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
+and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) =
+  let import = not hidden && item.ti_import in
+
   match item.ti_item with
   | Th_type (x, otyd) ->
-     replay_tyd ove (subst, ops, proofs, scope) (item.ti_import, x, otyd)
+     replay_tyd ove (subst, ops, proofs, scope) (import, x, otyd)
 
   | Th_operator (x, ({ op_kind = OB_oper _ } as oopd)) ->
-     replay_opd ove (subst, ops, proofs, scope) (item.ti_import, x, oopd)
+     replay_opd ove (subst, ops, proofs, scope) (import, x, oopd)
 
   | Th_operator (x, ({ op_kind = OB_pred _} as oopr)) ->
-     replay_prd ove (subst, ops, proofs, scope) (item.ti_import, x, oopr)
+     replay_prd ove (subst, ops, proofs, scope) (import, x, oopr)
 
   | Th_operator (x, ({ op_kind = OB_nott _} as oont)) ->
-     replay_ntd ove (subst, ops, proofs, scope) (item.ti_import, x, oont)
+     replay_ntd ove (subst, ops, proofs, scope) (import, x, oont)
 
   | Th_axiom (x, ax) ->
-     replay_axd ove (subst, ops, proofs, scope) (item.ti_import, x, ax)
+     replay_axd ove (subst, ops, proofs, scope) (import, x, ax)
 
   | Th_modtype (x, modty) ->
-     replay_modtype ove (subst, ops, proofs, scope) (item.ti_import, x, modty)
+     replay_modtype ove (subst, ops, proofs, scope) (import, x, modty)
 
   | Th_module me ->
-     replay_mod ove (subst, ops, proofs, scope) (item.ti_import, me)
+     replay_mod ove (subst, ops, proofs, scope) (import, me)
 
   | Th_export (p, lc) ->
-     replay_export ove (subst, ops, proofs, scope) (item.ti_import, p, lc)
+     replay_export ove (subst, ops, proofs, scope) (import, p, lc)
 
   | Th_baserw (x, lc) ->
-     replay_baserw ove (subst, ops, proofs, scope) (item.ti_import, x, lc)
+     replay_baserw ove (subst, ops, proofs, scope) (import, x, lc)
 
   | Th_addrw (p, l, lc) ->
-     replay_addrw ove (subst, ops, proofs, scope) (item.ti_import, p, l, lc)
+     replay_addrw ove (subst, ops, proofs, scope) (import, p, l, lc)
 
   | Th_reduction rules ->
-     replay_reduction ove (subst, ops, proofs, scope) (item.ti_import, rules)
+     replay_reduction ove (subst, ops, proofs, scope) (import, rules)
 
   | Th_auto at_base ->
-     replay_auto ove (subst, ops, proofs, scope) (item.ti_import, at_base)
+     replay_auto ove (subst, ops, proofs, scope) (import, at_base)
 
   | Th_typeclass (x, tc) ->
-     replay_typeclass ove (subst, ops, proofs, scope) (item.ti_import, x, tc)
+     replay_typeclass ove (subst, ops, proofs, scope) (import, x, tc)
 
   | Th_instance ((typ, ty), tc, lc) ->
-     replay_instance ove (subst, ops, proofs, scope) (item.ti_import, (typ, ty), tc, lc)
+     replay_instance ove (subst, ops, proofs, scope) (import, (typ, ty), tc, lc)
 
   | Th_theory (ox, cth) -> begin
       let thmode = cth.cth_mode in
       let (subst, x) = rename ove subst (`Theory, ox) in
       let subovrds = Msym.find_opt ox ove.ovre_ovrd.evc_ths in
-      let subovrds = EcUtils.odfl evc_empty subovrds in
+      let subovrds = EcUtils.odfl (evc_empty, false) subovrds in
+      let subovrds, clear = subovrds in
+      let hidden = hidden || clear in
       let subove   = { ove with
         ovre_ovrd     = subovrds;
         ovre_abstract = ove.ovre_abstract || (thmode = `Abstract);
@@ -1008,9 +1005,10 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
       let (subst, ops, proofs, subscope) =
         let subscope = ove.ovre_hooks.hthenter scope thmode x ove.ovre_local in
         let (subst, ops, proofs, subscope) =
-          List.fold_left (replay1 subove)
+          List.fold_left
+            (fun state item -> replay1 subove state (hidden, item))
             (subst, ops, proofs, subscope) cth.cth_items in
-        let scope = ove.ovre_hooks.hthexit subscope `Full in
+        let scope = ove.ovre_hooks.hthexit ~import:(not hidden) subscope `Full in
         (subst, ops, proofs, scope)
 
       in (subst, ops, proofs, subscope)
@@ -1019,7 +1017,7 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
 (* -------------------------------------------------------------------- *)
 let replay (hooks : 'a ovrhooks)
   ~abstract ~local ~incl ~clears ~renames
-  ~opath ~npath ovrds (scope : 'a) (name, items)
+  ~opath ~npath ovrds (scope : 'a) (name, hidden, items)
 =
   let subst = EcSubst.add_path EcSubst.empty ~src:opath ~dst:npath in
   let ove   = {
@@ -1039,9 +1037,10 @@ let replay (hooks : 'a ovrhooks)
     let mode  = if abstract then `Abstract else `Concrete in
     let scope = if incl then scope else hooks.hthenter scope mode name local in
     let _, _, proofs, scope =
-      List.fold_left (replay1 ove)
+      List.fold_left
+        (fun state item -> replay1 ove state (hidden, item))
         (subst, Mp.empty, [], scope) items in
-     let scope = if incl then scope else hooks.hthexit scope `No in
+     let scope = if incl then scope else hooks.hthexit scope ~import:true `No in
     (List.rev proofs, scope)
 
   with EcEnv.DuplicatedBinding x ->
diff --git a/src/ecTheoryReplay.mli b/src/ecTheoryReplay.mli
index 5afd716ba..9f795ef2e 100644
--- a/src/ecTheoryReplay.mli
+++ b/src/ecTheoryReplay.mli
@@ -25,9 +25,9 @@ type 'a ovrenv = {
 
 and 'a ovrhooks = {
   henv      : 'a -> EcSection.scenv;
-  hadd_item : 'a -> EcTheory.import -> EcTheory.theory_item_r -> 'a;
+  hadd_item : 'a -> import:bool -> EcTheory.theory_item_r -> 'a;
   hthenter  : 'a -> thmode -> symbol -> EcTypes.is_local -> 'a;
-  hthexit   : 'a -> [`Full | `ClearOnly | `No] -> 'a;
+  hthexit   : 'a -> import:bool -> [`Full | `ClearOnly | `No] -> 'a;
   herr      : 'b . ?loc:EcLocation.t -> string -> 'b;
 }
 
@@ -36,5 +36,5 @@ val replay : 'a ovrhooks
   -> abstract:bool -> local:is_local -> incl:bool
   -> clears:Sp.t -> renames:(renaming list)
   -> opath:path -> npath:path -> evclone
-  -> 'a -> symbol * theory_item list
-  ->  axclone list * 'a
+  -> 'a -> symbol * bool * theory_item list
+  -> axclone list * 'a
diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec
index cb439f187..c1a6e1fa4 100644
--- a/theories/algebra/PolyReduce.ec
+++ b/theories/algebra/PolyReduce.ec
@@ -11,10 +11,9 @@ abstract theory PolyReduce.
 
 clone import PolyComRing as BasePoly with
   (* We currently don't care about inverting polynomials *)
-  pred PolyComRing.unit <= fun p => exists q, q * p = oner,
-  op PolyComRing.invr <= fun p => choiceb (fun q => q * p = oner) p
-  proof PolyComRing.mulVr, PolyComRing.unitP, PolyComRing.unitout
-  remove abbrev (+) remove abbrev ( * ) remove abbrev [-].
+  pred PolyComRing.unit <= fun p => exists q, polyM q p = oner,
+  op PolyComRing.invr <= fun p => choiceb (fun q => polyM q p = oner) p
+  proof PolyComRing.mulVr, PolyComRing.unitP, PolyComRing.unitout.
 realize PolyComRing.mulVr by smt(choicebP).
 realize PolyComRing.unitP by smt().
 realize PolyComRing.unitout by smt(choiceb_dfl).