anchor.diff:        in
         let t =
             mk (Tm_match(t,
  -                       BU.map_opt asc_opt (close_ascription cfg env),
  +                       close_match_returns cfg env asc_opt,
                          branches |> List.map (close_one_branch env),
                          lopt)) t.pos
         in
  
positive.code:                           scrutinee //scrutinee was only reduced to wnf; reduce it fully
                  else scrutinee
                in
                let asc_opt = BU.map_opt asc_opt norm_ascription in
                let branches = norm_branches() in
                rebuild cfg env stack (mk (Tm_match(scrutinee, asc_opt, branches, lopt)) r)
            in
  
negative.code:                 log cfg  (fun () -> BU.print_string "+++ Keeping ascription \n");
                  let t1 = norm cfg env [] t1 in
                  log cfg  (fun () -> BU.print_string "+++ Normalizing ascription \n");
                  let asc = norm_ascription cfg env (tc, tacopt) in
                  match stack with
                  | Cfg (cfg', dbg) :: stack ->
                    maybe_debug cfg t1 dbg;
                    let t = mk (Tm_ascribed(U.unascribe t1, asc, l)) t.pos in
                    norm cfg' env stack t
                  | _ ->
                    rebuild cfg env stack (mk (Tm_ascribed(U.unascribe t1, asc, l)) t.pos)
              end
  
            | Tm_match(head, asc_opt, branches, lopt) ->
  