diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst
index 8554a846f6d..bda2a1dce32 100644
--- a/src/extraction/FStar.Extraction.ML.Modul.fst
+++ b/src/extraction/FStar.Extraction.ML.Modul.fst
@@ -756,6 +756,8 @@ let mark_sigelt_erased (se:sigelt) (g:uenv) : uenv =
 let fixup_sigelt_extract_as se =
   match se.sigel, find_map se.sigattrs N.is_extract_as_attr with
   | Sig_let {lids; lbs=(_, [lb])}, Some impl ->
+    // The specified implementation can be recursive,
+    // to be on the safe side we always mark the replaced sigelt as recursive.
     {se with sigel = Sig_let {lids; lbs=(true, [{lb with lbdef = impl}])}}
   | _ -> se
 
diff --git a/ulib/FStar.ExtractAs.fst b/ulib/FStar.ExtractAs.fst
index 9e5996bc959..11a785dafac 100644
--- a/ulib/FStar.ExtractAs.fst
+++ b/ulib/FStar.ExtractAs.fst
@@ -31,5 +31,7 @@ open FStar.Stubs.Reflection.Types
     and most likely cause the extracted program to crash.
 
     Note that the argument needs to be a literal quotation.
+    The implementation can be recursive,
+    but then you need to construct the attribute via a tactic.
  *)
 let extract_as (impl: term) = ()