diff --git a/src/tls13utils.rs b/src/tls13utils.rs index 339270c..e0db6e9 100644 --- a/src/tls13utils.rs +++ b/src/tls13utils.rs @@ -314,6 +314,7 @@ impl core::ops::Index for Bytes { } } +/// This is needed only for hax, so should likely be guarded by a feature flag. #[hax_lib::fstar::before( interface, "[@@ FStar.Tactics.Typeclasses.tcinstance]