anchor.diff:              then failwith (BU.format2 "(%s) CheckNoUvars: Unexpected unification variable remains: %s"
                                       (Range.string_of_range t.pos)
                                       (Print.term_to_string t))
  -            else rebuild cfg env stack t
  +            else rebuild cfg env stack (inline_closure_env cfg env [] t)
   
             | _ ->
               norm cfg env stack t
  
positive.code:                         (Print.term_to_string t))
               | _ ->
                inline_closure_env cfg env stack t
          else rebuild_closure cfg env stack t //should be closed anyway
  
        | Tm_type u ->
          let t = mk (Tm_type (norm_universe cfg env u)) t.pos in
  
negative.code:       | Tm_fvar _ ->
          rebuild_closure cfg env stack t
  
        | Tm_uvar (uv, s) ->
          if cfg.steps.check_no_uvars
          then let t = compress t in
               match t.n with
  