From a9d10039fd11a61b5412e0b18a3ee1013914e695 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 29 Apr 2019 18:18:22 +0200
Subject: [PATCH] [rmtmps] fix bug introduced in MR 1930 (marking unused
fc_builtins as being referenced)
---
src/kernel_internals/typing/rmtmps.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index e22c8830104..6b87bdf9097 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
| _ ->
--
GitLab