anchor.diff:                     || S.fv_eq_lid f PC.false_lid)
                   then false
                   else begin
  -                  match cfg.steps |> List.tryFind (function UnfoldOnly _ | UnfoldAttr _ -> true | _ -> false) with
  -                  | Some _ ->
  +                  if not (Option.isSome cfg.steps.unfold_only) || Option.isSome cfg.steps.unfold_attr
  +                  then
                       let attr_eq a a' = match U.eq_tm a a' with | U.Equal -> true | _ -> false in
  -                    should_delta && List.fold_left (fun acc x ->
  -                      match x with
  -                      | UnfoldOnly lids -> acc || BU.for_some (fv_eq_lid f) lids
  -                      | UnfoldAttr attr -> begin
  -                        match lookup_attrs_of_lid cfg.tcenv f.fv_name.v with
  -                        | Some attrs -> acc || BU.for_some (attr_eq attr) attrs
  -                        | _ -> acc
  -                        end
  -                      | _ -> acc) false cfg.steps
  -                  | _ -> should_delta
  +                    should_delta &&
  +                    (match cfg.steps.unfold_only with
  +                     | None -> true
  +                     | Some lids -> BU.for_some (fv_eq_lid f) lids) &&
  +                    (match cfg.steps.unfold_attr with
  +                     | None -> true
  +                     | Some attr -> begin match lookup_attrs_of_lid cfg.tcenv f.fv_name.v with
  +                                    | Some attrs -> BU.for_some (attr_eq attr) attrs
  +                                    | None -> true
  +                                    end)
  +                  else should_delta
                   end
               in
   
  
positive.code: let rec closure_as_term cfg (env:env) t =
      log cfg  (fun () -> BU.print2 ">>> %s Closure_as_term %s\n" (Print.tag_of_term t) (Print.term_to_string t));
      match env with
          | [] when not <| List.contains CompressUvars cfg.steps -> t
          | _ ->
          let t = compress t in
          match t.n with
  
negative.code:             norm cfg env stack head
  
            | Tm_refine(x, f) -> //non tail-recursive; the alternative is to keep marks on the stack to rebuild the term ... but that's very heavy
              if cfg.steps.weak
              then match env, stack with
                      | [], [] -> //TODO: Make this work in general!
                        let t_x = norm cfg env [] x.sort in
  