diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index e22c883010414384126989c604b625b02faefc05..6b87bdf9097cb33885ed36b48eda26c80cbe342e 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -609,9 +609,11 @@ class markReferencedVisitor = object
     | GVarDecl (varinfo, loc)
     | GFunDecl (_,varinfo, loc)
     | GFun ({svar = varinfo}, loc) ->
-      Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
-      Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
-      varinfo.vreferenced <- true;
+      if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then begin
+        Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
+        Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
+        varinfo.vreferenced <- true;
+      end;
       DoChildren
     | GAnnot _ -> DoChildren
     | _ ->