anchor.diff:  
       let imp_binders = tps @ indices |> List.map (fun (x, _) -> x, Some S.imp_tag) in
   
  +    let early_prims_inductive =
  +      lid_equals C.prims_lid  (Env.current_module env) &&
  +      (tc.ident.idText = "dtuple2" || List.existsb (fun s -> s = tc.ident.idText) early_prims_inductives)
  +    in
  +
       let discriminator_ses =
           if fvq <> Data_ctor
           then [] // We do not generate discriminators for record types
  
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 *)
  