anchor.diff:  (******************************************************************************)
   
   //for these types we don't generate projectors, discriminators, and hasEq axioms
  -let early_prims_inductives = [ "c_False"; "c_True"; "equals"; "h_equals"; "c_and"; "c_or"; "dtuple2" ]
  +let early_prims_inductives = [ "c_False"; "c_True"; "equals"; "h_equals"; "c_and"; "c_or" ]
   
   let mk_discriminator_and_indexed_projectors iquals                   (* Qualifiers of the envelopping bundle    *)
                                               (fvq:fv_qual)            (*                                         *)
  
positive.code:             let discriminator_name = U.mk_discriminator lid in
              let no_decl = false in
              let only_decl =
                    (lid_equals C.prims_lid  (Env.current_module env) && List.existsb (fun s -> s = tc.ident.idText) early_prims_inductives) ||
                    Options.dont_gen_projectors (Env.current_module env).str
              in
              let quals =
                  (* KM : What about Logic ? should it still be there even with an implementation *)
  
negative.code:           let field_name, _ = U.mk_field_projector_name lid x i in
            let t = SS.close_univ_vars uvs <| U.arrow binders (S.mk_Total (Subst.subst subst x.sort)) in
            let only_decl =
              early_prims_inductive ||
              Options.dont_gen_projectors (Env.current_module env).str
            in
            (* KM : Why would we want to prevent a declaration only in this particular case ? *)
            (* TODO : If we don't want the declaration then we need to propagate the right types in the patterns *)
  