anchor.diff:  
         | Tm_ascribed(t1, asc, _) ->
           maybe_weakly_reduced t1
  -        || (match fst asc with
  +        || (let asc_tc, asc_tac, _ = asc in
  +           (match asc_tc with
               | Inl t2 -> maybe_weakly_reduced t2
               | Inr c2 -> aux_comp c2)
  -        || (match snd asc with
  -           | None -> false
  -           | Some tac -> maybe_weakly_reduced tac)
  +           ||
  +           (match asc_tac with
  +            | None -> false
  +            | Some tac -> maybe_weakly_reduced tac))
   
         | Tm_meta(t, m) ->
           maybe_weakly_reduced t
  
positive.code:     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}
  
negative.code:                  let t = arrow (norm_binders cfg env bs) c in
                   rebuild cfg env stack t
  
            | Tm_ascribed(t1, _, l) when cfg.steps.unascribe ->
              norm cfg env stack t1
  
            | Tm_ascribed(t1, asc, l) ->
              begin match stack with
                | Match _ :: _
                | Arg _ :: _
  