Merge pull request #1322 from cryspen/rand-core-traits

Proof libs (F*): fix trait inheritance in rand-core
cryspen · Feb 21, 2025 · 72a2a92 · 72a2a92
2 parents 81f9b2f + 06c5205
commit 72a2a92
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/proof-libs/fstar/core/Rand_core.fsti b/proof-libs/fstar/core/Rand_core.fsti
@@ -8,10 +8,14 @@ class t_RngCore (t_Self: Type0) = {
 }
 
 class t_CryptoRng (t_Self: Type0) = {
+  [@@@FStar.Tactics.Typeclasses.tcinstance]
+  _super_core: t_RngCore t_Self;
   marker_trait: unit
 }
 
 class t_CryptoRngCore (t_Self: Type0) = {
+  [@@@FStar.Tactics.Typeclasses.tcinstance]
+  _super_crypto: t_CryptoRng t_Self;
   f_rngcore: t_Self -> t_Self
 }