diff --git a/case_studies/dot_product/dot.ml b/case_studies/dot_product/dot.ml
index 2f0564085..e9f0eba12 100644
--- a/case_studies/dot_product/dot.ml
+++ b/case_studies/dot_product/dot.ml
@@ -18,13 +18,7 @@ let part = 1 (* Choose which part you want to work on. *)
 let _ = if part = 1 then Run.script_cpp (fun () ->
   (* !! Function.elim_infix_ops ~indepth:true []; *)
   !! Loop.tile (int 32) ~index:"bi" ~bound:TileDivides [cFor "i"];
-
-  (* LATER: !! Variable.local_name ~var:"s" ~local_var:"t" [tSpanSeq [cForBody "bi"]]; *)
-  !! (
-    Sequence.intro ~mark:"t_scope" ~start:[tFirst; cForBody "bi"] ~stop:[tLast; cForBody "bi"] ();
-    Variable.local_name ~var:"s" ~local_var:"t" [cMark "t_scope"];
-    Sequence.elim [cMark "t_scope"];
-  );
+  !! Variable.local_name ~var:"s" ~local_var:"t" [tSpanSeq [cForBody "bi"]];
 
   (* DEPRECATED? !! Sequence_basic.insert (trm_let (new_var "d", typ_f32) (trm_get (trm_find_var "s" []))) [tFirst; cForBody "bi"]; *)
   !! (
diff --git a/doc/odoc_extra.css b/doc/odoc_extra.css
index aac9d9cac..5254e523c 100644
--- a/doc/odoc_extra.css
+++ b/doc/odoc_extra.css
@@ -23,6 +23,8 @@ body {
    /*border: 1px solid black;*/
    padding: 3px 5px 3px 5px;
    background: #FFFFA0;
+   color: #1a1a1a; /* anchor text dark: odoc's theme flips text to light in dark mode,
+                      which would be unreadable on the light-yellow background */
    font-weight: bold;
 }
 
@@ -83,3 +85,31 @@ body {
 .d2h-code-line del, .d2h-code-side-line del {
     background-color: inherit;
 }
+
+/* Dark-mode support.
+   odoc's stylesheet flips page text to a light color under
+   `prefers-color-scheme: dark` (see _doc/odoc.support/odoc.css), but the injected
+   example/diff blocks pin light backgrounds. Without the rules below you get
+   light-on-light (unreadable). odoc_extra.css is loaded after odoc.css and these
+   selectors are at least as specific, so they win without !important. */
+@media (prefers-color-scheme: dark) {
+
+  /* Example OCaml block: turn it into a proper dark code card instead of the
+     light-yellow highlight, keeping a faint yellow tint for identity. */
+  .code-unit-test {
+    background: #3a3a26;
+    color: #f5f1c0;
+  }
+
+  /* Diff block: diff2html hardcodes light pastel backgrounds for added/removed
+     lines that can't be re-tinted cleanly. Rather than override each one, we
+     force the whole diff into a light "island": a white table background (which
+     fills the transparent context-line cells) and dark inherited text (which
+     cascades to every cell while the changed lines keep their own pastels). */
+  .diff-unit-test .d2h-wrapper,
+  .diff-unit-test .d2h-file-wrapper,
+  .diff-unit-test .d2h-diff-table {
+    background: #ffffff;
+    color: #1a1a1a;
+  }
+}
diff --git a/lib/framework/flags.ml b/lib/framework/flags.ml
index 28132a5d7..7ddf0824b 100644
--- a/lib/framework/flags.ml
+++ b/lib/framework/flags.ml
@@ -21,6 +21,7 @@ let analyse_stats_details : bool ref = ref false
 (** [dump_ast_details]: flag to dump OptiTrust AST, both in the form of a '.ast' and '_enc.cpp' files. *)
 let dump_ast_details : bool ref = ref false
 
+(* TODO : deprecate once optilambda surface display works *)
 (** [pretty_matrix_notation]: flag to display matrix macros with syntactic sugar:
   MALLOC2(n, m, sizeof(T)) --> malloc(sizeof(T[n][m]))
   x[MINDEX2(n, m, i, j)] --> x[i;j]
@@ -124,16 +125,20 @@ let set_optilambda_repr repr =
    This allows for the propagation of the backtrace. *)
 let stop_on_first_resource_error = ref true
 
+(* TODO Yanni : reevaluate *)
 (** [resource_typing_enabled]: if false, never attempt typing resources and never introduce ghosts. *)
 let resource_typing_enabled = ref true
 
+(* TODO Yanni : reevaluate *)
 (** [check_validity]: perform validation of transformations *)
 let check_validity = ref false
 
+(* TODO Yanni : reevaluate *)
 (** [preserve_specs_only]: allow code transformation that preserve the specification without necessarily preserving the semantics
     TODO: update code which was also using check_validity for this purpose *)
 let preserve_specs_only = ref false
 
+(* TODO Yanni : reevaluate *)
 (** [disable_resource_typing ()] should be called when using OptiTrust without resources. *)
 let disable_resource_typing () =
   resource_typing_enabled := false;
@@ -145,6 +150,7 @@ let reparse_between_steps = ref false
 (** [recompute_resources_between_steps]: always recompute resources between two steps *)
 let recompute_resources_between_steps = ref false
 
+(* TODO Yanni : depreciate - should always be true *)
 (** [use_resources_with_models]: use resources of the form "p ~~> v" instead of "p ~> Cell". In the long term, this flag should disappear as we should be able to unify those two modes into one, using clever syntactic sugar and unification features. *)
 let use_resources_with_models = ref false
 
@@ -265,6 +271,7 @@ let string_to_steps_selector (s:string) : steps_selector =
   | "all" -> Steps_all
   | _ -> failwith "invalid step selector, should be one of 'none', 'script', 'important', 'effectful', 'all'"
 
+(* TODO : the trace would be smaller once we share terms in the trace *)
 (* Options to control which steps are exported in the trace.
    Be careful that a step not exported cannot be viewed even in step diff mode. *)
 let save_steps : steps_selector option ref = ref None
diff --git a/lib/framework/prelude.ml b/lib/framework/prelude.ml
index 7dbd4c926..b99e7d483 100644
--- a/lib/framework/prelude.ml
+++ b/lib/framework/prelude.ml
@@ -7,72 +7,7 @@ include Contextualized_error
 include Mark
 include Target
 include Trm_pattern
-
-module Trm = struct
-  include Trm
-  (* short aliases *)
-  let var = trm_var
-  let struct_access = trm_struct_access
-  let array_access = trm_array_access
-  let get_stringreprid = trm_get_stringreprid
-
-  let pattern_var = trm_pattern_var
-end
-
-module ShowAt = Show.At
-
-let trm_seq_nobrace = Nobrace.trm_seq
-let trm_seq_nobrace_nomarks = Nobrace.trm_seq_nomarks
-
-type seq_component =
-  | Trm of trm
-  | TrmList of trm list
-  | TrmMlist of trm mlist
-  | Mark of mark
-  | MarkList of mark list
-  | SeqComponents of seq_component list
-
-let trm_seq_helper ?(annot : trm_annot option) ?(loc : location) ?(result: var option) ?(braces = true) (components: seq_component list) : trm =
-  let rec aux cs acc = List.fold_right (fun comp acc ->
-    match comp with
-    | Trm t -> Mlist.push_front t acc
-    | TrmList tl -> Mlist.merge (Mlist.of_list tl) acc
-    | TrmMlist tml -> Mlist.merge tml acc
-    | Mark "" -> acc
-    | Mark m -> Mlist.insert_mark_at 0 m acc
-    | MarkList ms -> Mlist.insert_marks_at 0 ms acc
-    | SeqComponents cs -> aux cs acc
-  ) cs acc in
-  let mlist = aux components (Mlist.empty ()) in
-  if braces then
-    trm_seq ?annot ?loc ?result mlist
-  else begin
-    assert (annot = None);
-    assert (loc = None);
-    trm_seq_nobrace ?result mlist
-  end
-
-let update_span_helper (span : Dir.span) (t_seq : trm) (f : trm mlist -> seq_component list) : trm =
-  let instrs, result = trm_inv ~error:"expected seq" trm_seq_inv t_seq in
-  if span.start >= span.stop then begin
-    t_seq
-  end else begin
-    let (span_instrs, instrs_after) = Mlist.split ~left_bias:false span.stop instrs in
-    let (instrs_before, span_instrs) = Mlist.split ~left_bias:true span.start span_instrs in
-    let new_span_components = f span_instrs in
-    trm_seq_helper ~annot:t_seq.annot ?result [
-      TrmMlist instrs_before;
-      SeqComponents new_span_components;
-      TrmMlist instrs_after;
-    ]
-  end
-
-let skip_includes (t : trm) : trm =
-  match trm_seq_inv t with
-  | Some (instrs, None) ->
-    let not_include = Mlist.filter (fun t -> not (trm_is_include t)) instrs in
-    trm_seq not_include
-  | _ -> failwith "skip_includes should be called on the root of the AST"
+include Seq_helper
 
 let rec find_var_filter_on (candidates : typ option varmap ref) (filter : var -> bool) (t : trm) : unit =
   let update_map v ty =
@@ -100,7 +35,7 @@ let find_var_filter ?(target : target = []) (filter : var -> bool) : var * typ o
   then find_var_filter_on candidates filter (skip_includes (Trace.ast ()))
   else List.iter (fun p ->
     find_var_filter_on candidates filter (Target.resolve_path p)
-  ) (resolve_target target);
+  ) (resolve_target_with_stringreprs_available target (Trace.ast ()));
   (* let candidates = Var_set.filter filter vars in *)
   match Var_map.cardinal !candidates with
   | 0 -> failwith "could not find variable in current AST variables" (* ": %s" (vars_to_string (Var_set.elements vars)) *)
diff --git a/lib/framework/runtime/trace.ml b/lib/framework/runtime/trace.ml
index 7d69ae7f6..7d0d57407 100644
--- a/lib/framework/runtime/trace.ml
+++ b/lib/framework/runtime/trace.ml
@@ -1428,7 +1428,7 @@ let failure_expected (h : exn -> bool) (f : unit -> unit) : unit =
 let resource_error_expected (f: unit -> unit): unit =
   failure_expected (function
   | Resource_computation.ResourceError _ -> true
-  | _ -> false) f
+  | _ -> false) (fun () -> f (); recompute_resources ())
 
 (** [apply f]: applies the transformation [f] to the current AST,
    and updates the current ast with the result of that transformation.
diff --git a/lib/framework/seq_helper.ml b/lib/framework/seq_helper.ml
new file mode 100644
index 000000000..ca721d278
--- /dev/null
+++ b/lib/framework/seq_helper.ml
@@ -0,0 +1,78 @@
+include Optitrust_utils
+include Optitrust_ast
+include Ast
+include Trm
+include Typ
+include Contextualized_error
+include Mark
+(* include Target *)
+include Trm_pattern
+
+module Trm = struct
+  include Trm
+  (* short aliases *)
+  let var = trm_var
+  let struct_access = trm_struct_access
+  let array_access = trm_array_access
+  let get_stringreprid = trm_get_stringreprid
+
+  let pattern_var = trm_pattern_var
+end
+
+(* module Show.At = Show.At *)
+
+let debug_path = true
+
+let trm_seq_nobrace = Nobrace.trm_seq
+let trm_seq_nobrace_nomarks = Nobrace.trm_seq_nomarks
+
+type seq_component =
+  | Trm of trm
+  | TrmList of trm list
+  | TrmMlist of trm mlist
+  | Mark of mark
+  | MarkList of mark list
+  | SeqComponents of seq_component list
+
+let trm_seq_helper ?(annot : trm_annot option) ?(loc : location) ?(result: var option) ?(braces = true) (components: seq_component list) : trm =
+  let rec aux cs acc = List.fold_right (fun comp acc ->
+    match comp with
+    | Trm t -> Mlist.push_front t acc
+    | TrmList tl -> Mlist.merge (Mlist.of_list tl) acc
+    | TrmMlist tml -> Mlist.merge tml acc
+    | Mark "" -> acc
+    | Mark m -> Mlist.insert_mark_at 0 m acc
+    | MarkList ms -> Mlist.insert_marks_at 0 ms acc
+    | SeqComponents cs -> aux cs acc
+  ) cs acc in
+  let mlist = aux components (Mlist.empty ()) in
+  if braces then
+    trm_seq ?annot ?loc ?result mlist
+  else begin
+    assert (annot = None);
+    assert (loc = None);
+    trm_seq_nobrace ?result mlist
+  end
+
+let update_span_helper (span : Dir.span) (t_seq : trm) (f : trm mlist -> seq_component list) : trm =
+  let instrs, result = trm_inv ~error:"expected seq" trm_seq_inv t_seq in
+  if span.start > span.stop then begin
+    failwith "update_span_helper: This span is impossible [%n; %n]" span.start span.stop
+  end else begin
+    let (span_instrs, instrs_after) = Mlist.split ~left_bias:false span.stop instrs in
+    let (instrs_before, span_instrs) = Mlist.split ~left_bias:true span.start span_instrs in
+    let new_span_components = f span_instrs in
+    trm_seq_helper ~annot:t_seq.annot ?result [
+      TrmMlist instrs_before;
+      SeqComponents new_span_components;
+      TrmMlist instrs_after;
+    ]
+  end
+
+let skip_includes (t : trm) : trm =
+  match trm_seq_inv t with
+  | Some (instrs, None) ->
+    let not_include = Mlist.filter (fun t -> not (trm_is_include t)) instrs in
+    trm_seq not_include
+  | _ -> failwith "skip_includes should be called on the root of the AST"
+
diff --git a/lib/framework/show.ml b/lib/framework/show.ml
index 23a36d34f..160a34966 100644
--- a/lib/framework/show.ml
+++ b/lib/framework/show.ml
@@ -8,7 +8,7 @@ include Style
      Show.trm ~msg:"foo:" t
      Show.trm ~msg:"foo:" tg
      Show.trm ~msg:"foo:" (Target.resolve_path p)
-     ShowAt.trm ~msg:"foo:" (Target.of_path p)
+     Show.At.trm ~msg:"foo:" (Target.of_path p)
 *)
 
 
@@ -113,7 +113,7 @@ let trm_text ?(msg : string option) ?(only_desc : bool = false) (t : trm) : unit
 
 
 
-(* DEPRECATED: use ShowAt.trm []
+(* DEPRECATED: use Show.At.trm []
 let ast ?(style = Default) ?(msg : string = "") () : unit =
   trm ~style ~msg (**:(add_linebreak msg)*) (Trace.ast ())
 *)
@@ -179,9 +179,9 @@ module At = struct
 
   (* Operations *)
 
-(* DEPRECATED: use ShowAt.trm []
+(* DEPRECATED: use Show.At.trm []
   let ast ?(msg : string = "") (tg : Target.target) : unit =
-    if tg <> [] then fail None "ShowAt.ast: can only be called on the root, with argument []";
+    if tg <> [] then fail None "Show.At.ast: can only be called on the root, with argument []";
     ast ~msg ()
     *)
 
@@ -399,5 +399,5 @@ type style = {
 *)
 
 (* = Show.trm ~style msg (Target.resolve_path p) *)
-(* = ShowAt.trm ~style msg (Target.of_path p) *)
+(* = Show.At.trm ~style msg (Target.of_path p) *)
 (* let current_ast_at_path ?(style = Display) ?(msg : string = "") (p : Path.path) : *)
diff --git a/lib/framework/target/constr.ml b/lib/framework/target/constr.ml
index 28ab76027..4e46f439b 100644
--- a/lib/framework/target/constr.ml
+++ b/lib/framework/target/constr.ml
@@ -13,6 +13,8 @@ exception Resolve_target_failure of string
 (* TODO deprecate this after Target.iter is used everywhere *)
 let old_resolution = ref false
 
+let debug_marks = true
+
 (******************************************************************************)
 (*                        Data structure for targets                          *)
 (******************************************************************************)
@@ -826,9 +828,12 @@ let rec check_constraint ~(incontracts:bool) (c : constr) (t : trm) : bool =
 
   | Constr_prim (pred_ty, pred_prim), Trm_prim (ty1, p1) ->
     pred_ty ty1 && pred_prim p1
+
   | Constr_mark (pred, _m), _ ->
     if !old_resolution then begin
       let t_marks = trm_get_marks t in
+      if debug_marks then
+        begin Printf.printf "check_constraint: marks of term are [%s]" (String.concat "; " t_marks) end;
       begin match t.desc with
       | Trm_seq (tl, _) ->
         (List.exists pred t_marks) || (List.fold_left (fun acc x -> (List.exists pred x) || acc) false (Mlist.get_marks tl))
diff --git a/lib/framework/target/path.ml b/lib/framework/target/path.ml
index f5ca65eeb..f9b7e3738 100644
--- a/lib/framework/target/path.ml
+++ b/lib/framework/target/path.ml
@@ -5,6 +5,7 @@ open Typ
 open Contextualized_error
 open Mark
 open Tools
+open Seq_helper
 
 (***********************************************************************************)
 (*                               Auxiliary functions                               *)
@@ -57,7 +58,6 @@ let apply_on_path (transfo : trm -> trm) (t : trm) (dl : path) : trm =
         (* trm_fail t *)
         path_fail dl "apply_on_path: Dir_before should not remain at this stage; probably the transformation was not expecting a target-between (tBefore, tAfter, ...)"
       | Dir_span _, _ ->
-        (* trm_fail t *)
         path_fail dl "apply_on_path: Dir_span should not remain at this stage; probably the transformation was not expecting a target-span (tSpan)"
       | Dir_seq_nth n, Trm_seq (tl, result) ->
         { t with desc = Trm_seq (Mlist.update_nth n aux tl, result) }
@@ -241,7 +241,15 @@ let resolve_path_and_ctx (dl : path) (t : trm) : trm * (trm list) =
       let loc = t.loc in
       begin match d, t.desc with
       | Dir_before _, _ -> trm_fail t "aux_on_path_rec: Dir_before should not remain at this stage"
-      | Dir_span _, _ -> trm_fail t "aux_on_path_rec: Dir_span should not remain at this stage"
+      | Dir_span {start; stop}, Trm_seq (instrs, result) ->
+        if start > stop then begin
+          trm_fail t (Printf.sprintf "aux_on_path_rec: Dir_span has an impossible span [%n; %n]" start stop)
+        end else begin
+          let (span_instrs, _instrs_after) = Mlist.split ~left_bias:false stop instrs in
+          let (_instrs_before, span_instrs) = Mlist.split ~left_bias:true start span_instrs in
+          let t_seq = trm_seq ?result span_instrs in
+          aux t_seq
+        end
       | Dir_seq_nth n, Trm_seq (tl, result) ->
         let tl = Mlist.to_list tl in
         (* DEPRECATED:
diff --git a/lib/transfo/loop.ml b/lib/transfo/loop.ml
index e085d18e6..9c00c1c5a 100644
--- a/lib/transfo/loop.ml
+++ b/lib/transfo/loop.ml
@@ -158,8 +158,8 @@ let%transfo hoist_alloc_loop_list
         (* Transfo_debug.path "p_nested" p_nested;
         Transfo_debug.path "p" p; *)
         Matrix_basic.simpl_access_of_access (target_of_path p);
-        (* ShowAt.trm ~msg:"t@p" (target_of_path p);
-        ShowAt.trm ~msg:"t@p" (target_of_path (p @ [Dir_arg_nth 1])); *)
+        (* Show.At.trm ~msg:"t@p" (target_of_path p);
+        Show.At.trm ~msg:"t@p" (target_of_path (p @ [Dir_arg_nth 1])); *)
         Matrix_basic.simpl_index_add (target_of_path (p @ [Dir_arg_nth 1]));
         Arith.(simpl_rec gather_rec (target_of_path (p @ [Dir_arg_nth 1])));
       ) [nbAny; cMark mark]
diff --git a/lib/transfo/variable_basic.ml b/lib/transfo/variable_basic.ml
index 519f52239..1c9e06c7e 100644
--- a/lib/transfo/variable_basic.ml
+++ b/lib/transfo/variable_basic.ml
@@ -1,5 +1,6 @@
 open Prelude
 
+let debug_transfo = true
 
 (** [fold ~at tg]: expects the target [tg] to point at a variable declaration,
       [at] - denotes a target where the folding is done. If empty the folding operation
@@ -157,7 +158,6 @@ let%transfo init_attach (tg : target) : unit =
   Trace.justif_always_correct ();
   Target.apply_at_target_paths_in_seq Variable_core.init_attach_at tg
 
-
 (** [local_name_on mark curr_var var_typ local_var t] declares a local
   variable [local_var] and replaces [curr_var] with [local_var] in [t].
     - [curr_var]: the replaced variable
@@ -167,12 +167,13 @@ let%transfo init_attach (tg : target) : unit =
   *)
 let local_name_on (curr_var : var) (var_typ : typ)
   ~(uninit_pre : bool) ~(uninit_post : bool)
-  (local_var : string) (t : trm) : trm =
+  (local_var : string) (span : Dir.span) (t : trm) : trm =
   let local_var = new_var local_var in
   let let_instr = trm_let_mut (local_var, var_typ) (trm_var_get ~typ:var_typ curr_var) in
   let set_instr = trm_set (trm_var ~typ:var_typ curr_var) (trm_var_get ~typ:var_typ local_var) in
-  let new_t = trm_subst_var curr_var (trm_var local_var) t in
-  trm_seq_nobrace_nomarks [let_instr; new_t; set_instr]
+  update_span_helper span t (fun span_instrs ->
+    let subst_span_instrs = Mlist.map (trm_subst_var curr_var (trm_var local_var)) span_instrs in
+    [Trm let_instr; TrmMlist subst_span_instrs; Trm set_instr])
 
 (** [local_name ~var var_typ ~local_var tg] declares a local
   variable [local_var] and replaces [var] with [local_var] in
@@ -185,24 +186,10 @@ let%transfo local_name ~(var : var) (var_typ : typ)
   ~(local_var : string) (tg : target) : unit =
   if (uninit_pre || uninit_post) then
     failwith "not implemented";
-  Target.iter (fun p -> Marks.with_fresh_mark_on p (fun m ->
-    Nobrace_transfo.remove_after (fun () ->
-      Target.apply_at_path (local_name_on var var_typ ~uninit_pre ~uninit_post local_var) p
-    );
-    if !Flags.check_validity && not !Flags.preserve_specs_only then begin
-      step_backtrack ~discard_after:true (fun () ->
-        let p = resolve_mark_exactly_one m in
-        Nobrace_transfo.remove_after (fun () ->
-        Target.apply_at_path (fun t ->
-          let (_, open_w, close_w) = Resource_trm.ghost_pair_hide
-            (Resource_formula.formula_cell_var ~mem_typ:Resource_formula.mem_typ_any ~typ:var_typ var) in
-          trm_seq_nobrace_nomarks [open_w; t; close_w]
-        ) p
-        );
-        Resources.ensure_computed_at p
-      )
-    end
-  )) tg
+  Target.iter (fun p ->
+    let (p_seq, span) = Path.extract_last_dir_span p in
+    Target.apply_at_path (local_name_on var var_typ ~uninit_pre ~uninit_post local_var span) p_seq)
+    tg
 
 (** [delocalize array_size neutral_element fold_operation tg]: expects the target [tg] to point to
     a block of code of the following form
diff --git a/print_dep.sh b/print_dep.sh
new file mode 100755
index 000000000..2965d1c85
--- /dev/null
+++ b/print_dep.sh
@@ -0,0 +1 @@
+odep dune lib/transfo | dot -Tsvg -o dependencies.svg; open dependencies.svg
diff --git a/tests/ast/demo_show.ml b/tests/ast/demo_show.ml
index 6e0813336..236e95aa8 100644
--- a/tests/ast/demo_show.ml
+++ b/tests/ast/demo_show.ml
@@ -5,21 +5,21 @@ let has_reference (t : trm) : bool =
   Trm.trm_get_cstyles t = [Reference]
 
 let _ = Run.script_cpp ~capture_show_in_batch:true (fun () ->
-  !! ShowAt.trm ~msg:"AST" [];
-  (*!! ShowAt.trm ~msg:"for trm" [cFor "i"]; --> need decoding of nonroot*)
+  !! Show.At.trm ~msg:"AST" [];
+  (*!! Show.At.trm ~msg:"for trm" [cFor "i"]; --> need decoding of nonroot*)
   (* TODO: ensure a deterministic printing of identifiers
-  !! ShowAt.(trm ~style:(Style.internal ())) ~msg:"var-trm-internal" [cVarDef "x"];
-  !! ShowAt.(trm ~style:(Style.internal ())) ~msg:"for-trm-internal" [cFor "i"];
+  !! Show.At.(trm ~style:(Style.internal ())) ~msg:"var-trm-internal" [cVarDef "x"];
+  !! Show.At.(trm ~style:(Style.internal ())) ~msg:"for-trm-internal" [cFor "i"];
   *)
   (* too verbose
-     !! ShowAt.(trm ~style:(Style.internal_ast ())) ~msg:"for-trm-internal-ast" [cFor "i"]; *)
-  !! ShowAt.(trm ~style:(Style.internal_ast_only_desc ())) ~msg:"for-trm-internal-desc" [cFor "i"];
-  !! ShowAt.desc ~msg:"desc" [cFor "i"];
-  !! ShowAt.typ ~msg:"typ" [nbAny; cVar "x"]; (* cInContracts *)
+     !! Show.At.(trm ~style:(Style.internal_ast ())) ~msg:"for-trm-internal-ast" [cFor "i"]; *)
+  !! Show.At.(trm ~style:(Style.internal_ast_only_desc ())) ~msg:"for-trm-internal-desc" [cFor "i"];
+  !! Show.At.desc ~msg:"desc" [cFor "i"];
+  !! Show.At.typ ~msg:"typ" [nbAny; cVar "x"]; (* cInContracts *)
   !! Marks.add "mymark1" [cForBody "i"; cVar "x"];
   !! Marks.add "mymark2" [cForBody "i"; cVar "x"];
-  !! ShowAt.marks ~msg:"marks" [cForBody "i"; cVar "x"];
-  !! ShowAt.cstyle ~msg:"cstyle-item" [nbAny; Constr_pred has_reference];
-  !! ShowAt.annot ~msg:"annot" [dRoot];
+  !! Show.At.marks ~msg:"marks" [cForBody "i"; cVar "x"];
+  !! Show.At.cstyle ~msg:"cstyle-item" [nbAny; Constr_pred has_reference];
+  !! Show.At.annot ~msg:"annot" [dRoot];
 
 )
diff --git a/tests/interact/interact.ml b/tests/interact/interact.ml
index 43811dca0..1c344a8d9 100644
--- a/tests/interact/interact.ml
+++ b/tests/interact/interact.ml
@@ -14,9 +14,9 @@ let _ = Run.script_cpp (fun () ->
 
   !! Label.add "m0" [cVarDef "a"];
   (* TODO: fix show term--
-  ShowAt.trm [cVarDef "a"];
-  ShowAt.trm [cVarDef "b"];
-  ShowAt.trm [tFirst; cFunBody "main"]; *)
+  Show.At.trm [cVarDef "a"];
+  Show.At.trm [cVarDef "b"];
+  Show.At.trm [tFirst; cFunBody "main"]; *)
 
 
   (* FOR TESTING: uncomment to test an incorrect path:
@@ -30,7 +30,7 @@ let _ = Run.script_cpp (fun () ->
 
   (* Showing operation with step at front *)
   !! Label.add "m1" [cVarDef "b"];
-  (* TODO: fix show term-- ShowAt.trm [cVarDef "a"]; *)
+  (* TODO: fix show term-- Show.At.trm [cVarDef "a"]; *)
   (* Showing operation with reparse *)
   !! Label.add "m2" [cVarDef "a"];
   (* Showing two operations at once *)
diff --git a/tests/interact/interact_traceview.ml b/tests/interact/interact_traceview.ml
index 3445b1f10..e8ddbed92 100644
--- a/tests/interact/interact_traceview.ml
+++ b/tests/interact/interact_traceview.ml
@@ -74,7 +74,7 @@ let _ = Run.script_cpp (fun _ ->
   !! Show.ast (); Show.ast ();
   *)
   (* Examples of show functions with output on stdout *)
-  (* !! ShowAt.trm []; *)
+  (* !! Show.At.trm []; *)
   bigstep "fourth part";
   (* Try task "View diff using internal syntax" *)
   !! Label.add "lab6" [cVarDef "a"];
diff --git a/tests/variable/local_name/variable_local_name.cpp b/tests/variable/local_name/variable_local_name.cpp
index 85c93e99e..fddcb2e92 100644
--- a/tests/variable/local_name/variable_local_name.cpp
+++ b/tests/variable/local_name/variable_local_name.cpp
@@ -62,7 +62,24 @@ void ko_scope() {
   __pure();
   int x = 0;
   int a = 0;
-  l: {
+  l: { a++; }
+}
+
+void ok3() {
+  __pure();
+  int a = 0;
+  for (int i = 0; i < 10; i++) {
     a++;
   }
 }
+
+void ok4() {
+  __pure();
+
+  int a = 0;
+  /*@ target__begin @*/
+  int b = 0;
+  a++;
+  /*@ target__end @*/
+  b++;
+}
diff --git a/tests/variable/local_name/variable_local_name.ml b/tests/variable/local_name/variable_local_name.ml
index 3f263fa27..9e6c11ec3 100644
--- a/tests/variable/local_name/variable_local_name.ml
+++ b/tests/variable/local_name/variable_local_name.ml
@@ -7,20 +7,24 @@ let _ = Run.script_cpp (fun _ ->
   !! Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ok1"; cFor "i"];
   !! Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ok2"; cLabel "l"];
 
-  !! Trace.failure_expected (fun _e -> true) (fun () ->
-    Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ko1"; cFor "i"];
-  );
-  !! Trace.failure_expected (fun _e -> true) (fun () ->
+  (* !! Trace.resource_error_expected (fun () -> *)
+  !! Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ko1"; cFor "i"];
+  (* ); *)
+  !! Trace.resource_error_expected (fun () ->
     Variable.local_name ~var:"b" ~local_var:"x" [cFunBody "ko1"; cFor "i"];
   );
-  !! Trace.failure_expected (fun _e -> true) (fun () ->
+  !! Trace.resource_error_expected (fun () ->
     Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ko2"; cLabel "l"]
   );
-  !! Trace.failure_expected (fun _e -> true) (fun () ->
+  !! Trace.resource_error_expected (fun () ->
     Variable.local_name ~var:"b" ~local_var:"x" [cFunBody "ko2"; cLabel "l"]
   );
 
   (* TODO: this triggers a renaming, should it throw an error instead? *)
   !! Variable.local_name ~var:"a" ~local_var:"x"
     [cFunBody "ko_scope"; cLabel "l"];
+
+  !! Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ok3"; tSpanSeq [cForBody "i"]];
+
+  !! Variable.local_name ~var:"a" ~local_var:"x" [cFunBody "ok4"; tSpan [tBefore; cVarDef "b"] [tAfter; sInstr "a++"]];
 )
diff --git a/tests/variable/local_name/variable_local_name_doc.ml b/tests/variable/local_name/variable_local_name_doc.ml
index 99fd46cca..614904409 100644
--- a/tests/variable/local_name/variable_local_name_doc.ml
+++ b/tests/variable/local_name/variable_local_name_doc.ml
@@ -3,5 +3,4 @@ open Prelude
 
 let _ = Run.script_cpp (fun _ ->
   !! Variable.local_name ~var:"x" ~local_var:"y" [cLabel "sec"];
-
 )
diff --git a/tests/variable/local_name/variable_local_name_exp.cpp b/tests/variable/local_name/variable_local_name_exp.cpp
index bbd0d7c3c..7e80338c1 100644
--- a/tests/variable/local_name/variable_local_name_exp.cpp
+++ b/tests/variable/local_name/variable_local_name_exp.cpp
@@ -32,12 +32,14 @@ void ko1() {
   for (int j = 0; j < 10; j++) {
     __strict();
     __smodifies("&a ~> Cell");
+    int x = a;
     for (int i = 0; i < j; i++) {
       __strict();
-      __smodifies("&a ~> Cell");
-      a++;
+      __smodifies("&x ~> Cell");
+      x++;
       b++;
     }
+    a = x;
   }
   int y = 0;
 }
@@ -46,7 +48,7 @@ void ko2() {
   __pure();
   int a = 0;
   int& b = a;
-l : {
+l: {
   a++;
   b++;
 }
@@ -57,7 +59,29 @@ void ko_scope() {
   __pure();
   int x = 0;
   int a = 0;
-  int x1 = a;
-l : { x1++; }
-  a = x1;
+  int x4 = a;
+l: { x4++; }
+  a = x4;
+}
+
+void ok3() {
+  __pure();
+  int a = 0;
+  for (int i = 0; i < 10; i++) {
+    __strict();
+    __smodifies("&a ~> Cell");
+    int x = a;
+    x++;
+    a = x;
+  }
+}
+
+void ok4() {
+  __pure();
+  int a = 0;
+  int x = a;
+  int b = 0;
+  x++;
+  a = x;
+  b++;
 }
diff --git a/tools/web_view/optitrust_trace.css b/tools/web_view/optitrust_trace.css
index a5c2d91f9..7415215e9 100644
--- a/tools/web_view/optitrust_trace.css
+++ b/tools/web_view/optitrust_trace.css
@@ -85,7 +85,10 @@ pre {
 }
 .step-invalid .step-title {
   background: var(--vscode-inputValidation-warningBackground, #fff4ce);
-  color: var(--vscode-inputValidation-warningForeground, #222222);
+  /* Dark themes define warningBackground (a dark brown) but often leave
+     warningForeground unset, so fall back to the editor foreground rather
+     than a hardcoded near-black that is unreadable on the dark background. */
+  color: var(--vscode-inputValidation-warningForeground, var(--vscode-editor-foreground, #222222));
 }
 .step-error .step-title {
   background: var(--vscode-inputValidation-errorBackground, #ff3333);