anchor.diff:        let s = [Beta; Zeta; Iota; Primops; UnfoldUntil Delta_constant; Reify] in
         Some (s, tm)
       | [(steps, _); _; (tm, _)] ->
  -      let add_exclude s z = if not (List.contains z s) then Exclude z::s else s in
  +      let add_exclude s z = if List.contains z s then s else Exclude z :: s in
         begin
         match parse_steps (full_norm steps) with
         | None -> None
  
positive.code:                              match attrs, cfg.steps.unfold_attr with
                               | None, Some _ -> false
                               | Some ats, Some ats' -> BU.for_some (fun at -> BU.for_some (attr_eq at) ats') ats
                               | _, _ -> false))
                   in
                   log cfg (fun () -> BU.print3 ">>> For %s (%s), should_delta = %s\n"
                                   (Print.term_to_string t)
  
negative.code:                          | Eager_unfolding_only -> true
                           | Unfold l -> Common.delta_depth_greater_than fv.fv_delta l)
                   in
                   let should_delta = should_delta && (
                            let attrs = Env.attrs_of_qninfo qninfo in
                             // never unfold something marked tac_opaque when reducing tactics
                            (not cfg.steps.unfold_tac ||
                             not (cases (BU.for_some (attr_eq U.tac_opaque_attr)) false attrs)) &&
  