anchor.diff:  
               | Pat_constant _c, Tm_constant c ->
   
  -              [U.mk_eq2 U_zero (tc_constant env pat_exp.pos c) (force_scrutinee()) pat_exp]
  +              [U.mk_decidable_eq (tc_constant env pat_exp.pos c) (force_scrutinee ()) pat_exp]
   
               | Pat_constant (FStar.Const.Const_int(_, Some _)), _ ->
                 //machine integer pattern, cf. #1572
  
positive.code:                         | None -> []  // We don't use the discriminator if we are typechecking it
                          | _ ->
                              let disc = S.fvar discriminator (Delta_equational_at_level 1) None in
                              let disc = mk_Tm_app disc [as_arg scrutinee_tm] scrutinee_tm.pos in
                              [U.mk_eq2 U_zero U.t_bool disc U.exp_true_bool]
                  else []
              in
  
  
negative.code:           Env.trivial_guard,
            false
  
          | Pat_constant c ->
            (*
             * AR: enforcing decidable equality, since the branch guards are in boolean now
             *     so whereas earlier we did scrutinee == c,
             *     we now have scrutinee = c, so we need decidable equality on c
             *)
            (match c with
             | Const_unit | Const_bool _ | Const_int _ | Const_char _ | Const_float _ | Const_string _ -> ()
             | _ ->
               fail (BU.format1
                       "Pattern matching a constant that does not have decidable equality: %s"
                       (Print.const_to_string c)));
            let _, e_c, _, _ = PatternUtils.pat_as_exp false env p in
            let e_c, lc, g = tc_tot_or_gtot_term env e_c in
            Rel.force_trivial_guard env g;
  