chore(radium): Remove dependency to rrconfig

rr_frontend/Cargo.lock

@@ -588,7 +588,6 @@ dependencies = [
  "derive_more 1.0.0-beta.6",
  "indent_write",
  "log",
- "rrconfig",
 ]
 
 [[package]]

rr_frontend/radium/Cargo.toml

@@ -8,8 +8,6 @@ repository.workspace = true
 version.workspace = true
 
 [dependencies]
-rrconfig.workspace = true
-
 derive_more.workspace = true
 indent_write.workspace = true
 log.workspace = true

rr_frontend/radium/src/code.rs

@@ -782,6 +782,7 @@ impl std::fmt::Display for InvariantMap {
 pub struct Function<'def> {
     pub code: FunctionCode,
     pub spec: FunctionSpec<'def>,
+
     /// Generic types in scope for this function
     generic_types: Vec<LiteralTyParam>,
 
@@ -1042,7 +1043,7 @@ impl<'def> Function<'def> {
         write!(f, "init_tyvars ({} ).\n", formatted_tyvars.as_str())
     }
 
-    pub fn generate_proof<F>(&self, f: &mut F) -> Result<(), io::Error>
+    pub fn generate_proof<F>(&self, f: &mut F, admit_proofs: bool) -> Result<(), io::Error>
     where
         F: io::Write,
     {
@@ -1081,7 +1082,7 @@ impl<'def> Function<'def> {
             write!(f, "Unshelve. all: print_remaining_sidecond.\n")?;
         }
 
-        if rrconfig::admit_proofs() {
+        if admit_proofs {
             write!(f, "Admitted. (* admitted due to admit_proofs config flag *)\n")?;
         } else {
             write!(f, "Qed.\n")?;

rr_frontend/translation/src/lib.rs

@@ -606,7 +606,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
                 )
                 .unwrap();
 
-            fun.generate_proof(&mut proof_file).unwrap();
+            fun.generate_proof(&mut proof_file, rrconfig::admit_proofs()).unwrap();
 
             proof_file.write("End proof.".as_bytes()).unwrap();
         }