anchor.diff:                    norm ({cfg with steps=s; primitive_steps=ps; delta_level=dl}) env stack t
   
                   | MemoLazy r :: stack ->
  -                  set_memo r (env, t); //We intentionally do not memoize the strong normal form; only the WHNF
  +                  set_memo cfg r (env, t); //We intentionally do not memoize the strong normal form; only the WHNF
                     log cfg  (fun () -> BU.print1 "\tSet memo %s\n" (Print.term_to_string t));
                     norm cfg env stack t
   
  
positive.code:               begin match lookup_bvar env x with
                      | Univ _ -> failwith "Impossible: term variable is bound to a universe"
                      | Dummy -> t
                      | Clos(env, t0, r, _) -> closure_as_term cfg env t0
                end
  
             | Tm_app(head, args) ->
  
negative.code:     let d = match d with
          | [] -> [Env.NoDelta]
          | _ -> d in
      {tcenv=e;
       steps=s;
       delta_level=d;
       primitive_steps=built_in_primitive_steps;
       strong=false;
       memoize_lazy=true}
  
  let normalize_with_primitive_steps ps s e t =
      let c = config s e in
  