anchor.diff:              else let us = UnivArgs(List.map (norm_universe cfg env) us, t.pos) in
                    let stack = us::stack in
                    norm cfg env stack t'
  -
  -          | Tm_fvar fv ->
  -            let qninfo = Env.lookup_qname cfg.tcenv (S.lid_of_fv fv) in
  -            begin match decide_unfolding cfg env stack t.pos fv qninfo with
  -            | Some (cfg, stack) -> do_unfold_fv cfg env stack t qninfo fv
  -            | None -> rebuild cfg env stack t
  -            end
   
             | Tm_bvar x ->
               begin match lookup_bvar env x with
  
positive.code:     let r_env = Env.set_range cfg.tcenv (S.range_of_fv f) in
      match Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo with
         | None ->
           log cfg (fun () -> // printfn "delta_level = %A, qninfo=%A" cfg.delta_level qninfo;
                           BU.print "Tm_fvar case 2\n" []) ;
           rebuild cfg env stack t0
  
         | Some (us, t) ->
           begin
           log cfg (fun () -> BU.print2 ">>> Unfolded %s to %s\n"
                         (Print.term_to_string t0) (Print.term_to_string t));
           let t =
             if cfg.steps.unfold_until = Some delta_constant
  
negative.code:     // We unfold dm4f actions if and only if we are reifying
      | _ when Env.qninfo_is_action qninfo ->
          let b = should_reify cfg stack in
          log_unfolding cfg (fun () -> BU.print2 " >> For DM4F action %s, should_reify = %s\n"
                                                 (Print.fv_to_string fv)
                                                 (string_of_bool b));
          if b then reif else no
  