anchor.diff:  (* This is used when computing WHNFs                               *)
   (*******************************************************************)
   let rec inline_closure_env cfg (env:env) stack t =
  -    log cfg (fun () -> BU.print2 ">>> %s Closure_as_term %s\n" (Print.tag_of_term t) (Print.term_to_string t));
  +    let t = compress t in
  +    log cfg (fun () -> BU.print3 "\n>>> %s (env=%s) Closure_as_term %s\n" (Print.tag_of_term t) (env_to_string env) (Print.term_to_string t));
       match env with
       | [] when not <| cfg.steps.compress_uvars ->
         rebuild_closure cfg env stack t
   
       | _ ->
  -      let t = compress t in
         match t.n with
         | Tm_delayed _ ->
           failwith "Impossible"
  
positive.code:     | UnivArgs _ -> "UnivArgs"
      | Match   _ -> "Match"
      | App (_, t,_,_) -> BU.format1 "App %s" (Print.term_to_string t)
      | Meta (m,_) -> "Meta"
      | Let  _ -> "Let"
      | Cfg _ -> "Cfg"
      | Debug (t, _) -> BU.format1 "Debug %s" (Print.term_to_string t)
  
negative.code:                     begin match m with
                        | Meta_labeled(l, r, _) ->
                          (* meta doesn't block reduction, but we need to put the label back *)
                          norm cfg env (Meta(env,m,r)::stack) head
  
                        | Meta_pattern args ->
                            let args = norm_pattern_args cfg env args in
                            norm cfg env (Meta(env,Meta_pattern args, t.pos)::stack) head //meta doesn't block reduction, but we need to put the label back
  
                        | _ ->
                            norm cfg env stack head //meta doesn't block reduction
  