anchor.diff:                              | _ -> true)
             in
             let simple_bvs, simple_pat_e, g0, simple_pat_elab =
  -              PatternUtils.pat_as_exp false env simple_pat
  +              PatternUtils.pat_as_exp false false env simple_pat
             in
             if List.length simple_bvs <> List.length sub_pats
             then failwith (BU.format4 "(%s) Impossible: pattern bvar mismatch: %s; expected %s sub pats; got %s"
  
positive.code:     let rec aux env us bs =
        match bs with
        | [] ->
          bind_opt (universe_of_well_typed_term env (U.comp_result c)) (fun uc ->
          Some (mk_tm_type (S.U_max (uc::us))))
  
        | ({binder_bv=x;binder_qual=imp})::bs ->
          // BU.print2 "type_of_well_typed_term computed universe of %s as : %s\n"
  
negative.code: 
    | Tm_ascribed(_, (Inl t, _), _) -> Some t
    | Tm_ascribed(_, (Inr c, _), _) -> Some (U.comp_result c)
    | Tm_uvar (u, s) ->
      // BU.print2 "type of well typed term %s, ctx uvar typ is %s\n"
      //   (Print.term_to_string t)
      //   (Print.term_to_string u.ctx_uvar_typ);
      Some (SS.subst' s u.ctx_uvar_typ)
  
    | Tm_quoted (tm, qi) ->
      Some (S.t_term)
  