diff --git a/proof-libs/fstar/core/Core.Default.fsti b/proof-libs/fstar/core/Core.Default.fsti
index 406cc0774..ebf53e0a7 100644
--- a/proof-libs/fstar/core/Core.Default.fsti
+++ b/proof-libs/fstar/core/Core.Default.fsti
@@ -1,5 +1,7 @@
 module Core.Default
 
 class t_Default (t: Type0) = {
-  v_default: unit -> t;
+  f_default_pre: unit -> Type0;
+  f_default_post: unit -> out:t -> Type0;
+  f_default: unit -> t;
 }