anchor.diff:  
               if not should_delta
               then rebuild cfg env stack t
  -            else let r_env = Env.set_range cfg.tcenv (S.range_of_fv f) in //preserve the range info on the returned def
  -                 begin match Env.lookup_definition cfg.delta_level r_env f.fv_name.v with
  -                    | None ->
  -                      log cfg (fun () -> BU.print "Tm_fvar case 2\n" []) ;
  -                      rebuild cfg env stack t
  -
  -                    | Some (us, t) ->
  -                      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 |> List.contains (UnfoldUntil Delta_constant)
  -                        //we're really trying to compute here; no point propagating range information
  -                        //which can be expensive
  -                        then t
  -                        else Subst.set_use_range (Ident.range_of_lid f.fv_name.v) t
  -                      in
  -                      let n = List.length us in
  -                      if n > 0
  -                      then match stack with //universe beta reduction
  -                             | UnivArgs(us', _)::stack ->
  -                               let env = us' |> List.fold_left (fun env u -> Univ u::env) env in
  -                               norm cfg env stack t
  -                             | _ when (cfg.steps |> List.contains EraseUniverses) ->
  -                               norm cfg env stack t
  -                             | _ -> failwith (BU.format1 "Impossible: missing universe instantiation on %s" (Print.lid_to_string f.fv_name.v))
  -                      else norm cfg env stack t
  -                 end
  +            else do_unfold_fv cfg env stack t f
   
             | Tm_bvar x ->
               begin match lookup_bvar env x with
  
positive.code:           | Tm_uvar _
            | Tm_constant _
            | Tm_name _
            | Tm_fvar( {fv_delta=Delta_constant} )
            | 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_app(hd, args)
              when U.is_fstar_tactics_embed hd
  
negative.code:                     rebuild cfg env stack t
                  end
          end
  
  and do_unfold_fv cfg env stack (t0:term) (f:fv) : term =
      //preserve the range info on the returned def
      let r_env = Env.set_range cfg.tcenv (S.range_of_fv f) in
      match Env.lookup_definition cfg.delta_level r_env f.fv_name.v with
         | None ->
           log cfg (fun () -> BU.print "Tm_fvar case 2\n" []) ;
           rebuild cfg env stack t0
  
         | Some (us, t) ->
           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 |> List.contains (UnfoldUntil Delta_constant)
             //we're really trying to compute here; no point propagating range information
             //which can be expensive
             then t
             else Subst.set_use_range (Ident.range_of_lid f.fv_name.v) t
           in
           let n = List.length us in
           if n > 0
           then match stack with //universe beta reduction
                  | UnivArgs(us', _)::stack ->
                    let env = us' |> List.fold_left (fun env u -> Univ u::env) env in
                    norm cfg env stack t
                  | _ when (cfg.steps |> List.contains EraseUniverses) ->
                    norm cfg env stack t
                  | _ -> failwith (BU.format1 "Impossible: missing universe instantiation on %s" (Print.lid_to_string f.fv_name.v))
           else norm cfg env stack t
  
  (* Reifies the lifting of the term [e] of type [t] from computational  *)
  (* effect [m] to computational effect [m'] using lifting data in [env] *)
  