case_studies/minivec/annotation_patch.patch

...udies/minivec/output/minivec/proofs/proof_RawVec_T_grow.v

case_studies/minivec/output/minivec/proofs/proof_Vec_T_pop.v

...nivec/output/minivec/proofs/proof_client_get_mut_client.v

.../tests/output/tests/proofs/proof_traits_foo_call_foobar.v

...tests/output/tests/proofs/proof_traits_foo_call_foobar2.v

...ies/tests/output/tests/proofs/proof_vec_client_init_vec.v

case_studies/tests/src/references.rs

rr_frontend/Cargo.toml

rr_frontend/radium/src/code.rs

rr_frontend/radium/src/coq.rs

rr_frontend/radium/src/specs.rs

...ranslation/src/environment/collect_prusti_spec_visitor.rs

rr_frontend/translation/src/environment/mod.rs

rr_frontend/translation/src/function_body.rs

rr_frontend/translation/src/lib.rs

rr_frontend/translation/src/shim_registry.rs

rr_frontend/translation/src/trait_registry.rs

rr_frontend/translation/src/type_translator.rs

theories/caesium/lang.v