diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index dcd72fea21d1534d5b73eda86ef8d2d596c7b2c8..b8c304afc7edc8b3159e8b376cab35322174bde2 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -29,7 +29,6 @@ rustflags = [
     # clippy::nursery
     "-Aclippy::empty_line_after_doc_comments",
     "-Aclippy::option_if_let_else",
-    "-Aclippy::redundant_pub_crate",
     "-Aclippy::string_lit_as_bytes",
     "-Aclippy::type_repetition_in_bounds",
     "-Aclippy::use_self",
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 6cf05898a96d898272ee7a2eb1b1f73e676970f9..80d0bd91db2cbf43ee9d8d39ae4e1c8d4252f213 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -163,7 +163,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for RRParam {
 
 /// Parse a list of comma-separated parameter declarations.
 #[derive(Debug)]
-pub(crate) struct RRParams {
+pub struct RRParams {
     pub(crate) params: Vec<RRParam>,
 }
 
@@ -177,7 +177,7 @@ impl<'a> Parse<ParseMeta<'a>> for RRParams {
     }
 }
 
-pub(crate) struct CoqPath(specs::CoqPath);
+pub struct CoqPath(specs::CoqPath);
 
 impl Into<specs::CoqPath> for CoqPath {
     fn into(self) -> specs::CoqPath {
@@ -256,7 +256,7 @@ pub fn str_err(e: parse::ParseError) -> String {
 pub type ParseMeta<'a> = (&'a [specs::LiteralTyParam], &'a [(Option<String>, specs::Lft)]);
 
 /// Handle escape sequences in the given string.
-pub(crate) fn handle_escapes(s: &str) -> String {
+pub fn handle_escapes(s: &str) -> String {
     let s = String::from(s);
     let s = s.replace("\\\"", "\"");
 
@@ -274,7 +274,7 @@ pub(crate) fn handle_escapes(s: &str) -> String {
 /// - `{st_of T}` is replaced by the syntactic type of the type parameter `T`
 /// - `{ly_of T}` is replaced by a term giving the layout of the type parameter `T`'s syntactic type
 /// - `{'a}` is replaced by a term corresponding to the lifetime parameter 'a
-pub(crate) fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, specs::TypeAnnotMeta) {
+pub fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, specs::TypeAnnotMeta) {
     let params = meta.0;
     let lfts = meta.1;
 
diff --git a/rr_frontend/translation/src/traits.rs b/rr_frontend/translation/src/traits.rs
index 5fb7fe02907a14fb7c7d0eb873b4728e53278ab5..a7899ed63264198b2b1626138f332a53ed52455f 100644
--- a/rr_frontend/translation/src/traits.rs
+++ b/rr_frontend/translation/src/traits.rs
@@ -9,7 +9,7 @@ use rustc_middle::ty::{
 };
 use rustc_trait_selection::traits::{ImplSource, NormalizeExt};
 
-pub(crate) fn associated_items(tcx: TyCtxt, def_id: DefId) -> impl Iterator<Item = &AssocItem> {
+pub fn associated_items(tcx: TyCtxt, def_id: DefId) -> impl Iterator<Item = &AssocItem> {
     tcx.associated_items(def_id).in_definition_order()
 }
 
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 2445414ead7dcf3a9cebbdf775cf9fa3cbe651e9..56d61ad94eb9a60fb8cac9b3a6360e765a8ec8b7 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -25,7 +25,7 @@ use crate::tyvars::*;
 
 /// Strip symbols from an identifier to be compatible with Coq.
 /// In particular things like ' or ::.
-pub(crate) fn strip_coq_ident(s: &str) -> String {
+pub fn strip_coq_ident(s: &str) -> String {
     let s = str::replace(s, "'", "");
     let s = str::replace(&s, "::", "_");
     let s = s.replace(|c: char| !(c.is_alphanumeric() || c == '_'), "");
@@ -41,7 +41,7 @@ pub type FnGenericKey<'tcx> = Vec<ty::Ty<'tcx>>;
 /// Keys used to deduplicate adt uses for syn_type assumptions.
 /// TODO maybe we should use SimplifiedType + simplify_type instead of the syntys?
 #[derive(Eq, PartialEq, Hash, Debug)]
-pub(crate) struct AdtUseKey {
+pub struct AdtUseKey {
     pub base_did: DefId,
     pub generics: Vec<radium::SynType>,
 }