anchor.diff:      match BU.find_opt (fun y -> (text_of_id y.ppname = text_of_id x)) l with
       | Some y -> l, e, y
       | _ ->
  -      let e, x = push_bv e x in
  -      (x::l), e, x
  +      let e, xbv = push_bv e x in
  +      (xbv::l), e, xbv
     in
   
     let rec aux' (top:bool) (loc:lenv_t) (env:env_t) (p:pattern)
  
positive.code:             let r = Range.union_ranges hd.p tl.p in
              pos_r r <| Pat_cons(S.lid_as_fv C.cons_lid delta_constant (Some Data_ctor), [(hd, false);(tl, false)])) pats
                          (pos_r (Range.end_range p.prange) <| Pat_cons(S.lid_as_fv C.nil_lid delta_constant (Some Data_ctor), [])) in
          let x = S.new_bv (Some p.prange) tun in
          loc, env, LocalBinder(x, None), pat, annots
  
        | PatTuple(args, dep) ->
  
negative.code:         let l = match constr.n with
            | Tm_fvar fv -> fv
            | _ -> failwith "impossible" in
          let x = S.new_bv (Some p.prange) (tun_r p.prange) in
          loc, env, LocalBinder(x, None), pos <| Pat_cons(l, args), annots
  
        | PatRecord ([]) ->
  