anchor.diff:      | _, Some _, _, _
       | _, _, Some _, _
       | _, _, _, Some _ ->
  +        log_unfolding cfg (fun () -> BU.print1 ">>> Reached a %s with selective unfolding\n"
  +                                               (Print.fv_to_string fv));
           comb_or [
            (match cfg.steps.unfold_only with
             | None -> yes
  
positive.code:     {tcenv=e;
       debug = { gen = Env.debug e (Options.Other "Norm")
               ; primop = Env.debug e (Options.Other "Primops")
               ; b380 = Env.debug e (Options.Other "380")
               ; wpe  = Env.debug e (Options.Other "WPE")
               ; norm_delayed = Env.debug e (Options.Other "NormDelayed")
  
negative.code: 
  let log_primops cfg f =
      if cfg.debug.primop then f () else ()
  
  let log_unfolding cfg f =
      if cfg.debug.unfolding then f () else ()
  
  let is_empty = function
      | [] -> true
  