aboutsummaryrefslogtreecommitdiffstats
path: root/common/Sections.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-02-06 16:53:12 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2017-02-06 16:53:12 +0100
commit8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed (patch)
tree43e89a45ed321081cbcaaac06165a7e62b84a34b /common/Sections.mli
parent9d4bb7ec914566b3920cca3c6823515448fb65c1 (diff)
parent4afaf8c23274752c8a6067bd785e114578068702 (diff)
downloadcompcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.tar.gz
compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.zip
Merge branch 'elaboration-of-attributes'
Diffstat (limited to 'common/Sections.mli')
-rw-r--r--common/Sections.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Sections.mli b/common/Sections.mli
index 8a13fb8a..b83b0bb4 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -47,5 +47,5 @@ val use_section_for: AST.ident -> string -> bool
val for_variable: Env.t -> AST.ident -> C.typ -> bool ->
section_name * access_mode
-val for_function: Env.t -> AST.ident -> C.typ -> section_name list
+val for_function: Env.t -> AST.ident -> C.attributes -> section_name list
val for_stringlit: unit -> section_name