anchor.diff:          if cfg.steps.iota
           then matches scrutinee branches
           else norm_and_rebuild_match ()
  +
  +and norm_match_returns cfg env ret_opt =
  +  match ret_opt with
  +  | None -> None
  +  | Some (b, asc) ->
  +    let b = norm_binder cfg env b in
  +    let subst, asc = SS.open_ascription [b] asc in
  +    let asc = norm_ascription cfg (dummy::env) asc in
  +    Some (b, SS.close_ascription subst asc)
  +
  +and norm_ascription cfg env (tc, tacopt) =
  +  (match tc with
  +   | Inl t -> Inl (norm cfg env [] t)
  +   | Inr c -> Inr (norm_comp cfg env c)),
  +  BU.map_opt tacopt (norm cfg env [])
   
   and norm_residual_comp cfg env (rc:residual_comp) : residual_comp =
     {rc with residual_typ = BU.map_option (closure_as_term cfg env) rc.residual_typ}
  
positive.code:             then closure_as_term cfg_exclude_zeta env t
              else norm cfg_exclude_zeta env [] t
            in
            let norm_ascription (tc, tacopt) =
              let tc = match tc with
                       | Inl t -> Inl (norm cfg env [] t)
                       | Inr c -> Inr (norm_comp cfg env c) in
              let tacopt = BU.map_opt tacopt (norm cfg env []) in
              tc, tacopt in
            let rec norm_pat env p = match p.v with
              | Pat_constant _ -> p, env
              | Pat_cons(fv, pats) ->
  
negative.code: 
      | _ -> failwith "Impossible: unexpected stack element"
  
  
  and close_match_returns cfg env ret_opt =
    match ret_opt with
    | None -> None
    | Some (b, asc) ->
      let bs, env = close_binders cfg env [b] in
      let asc = close_ascription cfg env asc in
      Some (List.hd bs, asc)
  
  and close_ascription cfg env (annot, tacopt) =
    let annot =
  