anchor.diff:               | Eager_unfolding_only -> true
                | Unfold l -> Common.delta_depth_greater_than fv.fv_delta l))
       in
  -    log_unfolding cfg (fun () -> BU.print3 ">>> For %s (%s), unfolding res = %s\n"
  +    log_unfolding cfg (fun () -> BU.print3 " >> For %s (%s), unfolding res = %s\n"
                       (Print.fv_to_string fv)
                       (Range.string_of_range rng)
                       (string_of_res res));
  
positive.code: 
            | Tm_lazy _
  
            | Tm_fvar( {fv_delta=Delta_constant_at_level 0} )
            | Tm_fvar( {fv_qual=Some Data_ctor } )
            | Tm_fvar( {fv_qual=Some (Record_ctor _)} ) -> //these last three are just constructors; no delta steps can apply
              //log cfg (fun () -> BU.print "Tm_fvar case 0\n" []) ;
              rebuild cfg env stack t
  
            | Tm_quoted _ ->
              rebuild cfg env stack (closure_as_term cfg env t)
  
negative.code:         // Unfolding fully, use new cfg with more steps and keep old one in stack
          let cfg' =
              { cfg with steps = { cfg.steps with
                         unfold_only  = None
                       ; unfold_fully = None
                       ; unfold_attr  = None
                       ; unfold_until = Some delta_constant } } in
          let stack' = (Cfg cfg) :: stack in
          Some (cfg', stack')
  