aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/GCC.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 /cparser/GCC.mli
parent9d4bb7ec914566b3920cca3c6823515448fb65c1 (diff)
parent4afaf8c23274752c8a6067bd785e114578068702 (diff)
downloadcompcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.tar.gz
compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.zip
Merge branch 'elaboration-of-attributes'
Diffstat (limited to 'cparser/GCC.mli')
-rw-r--r--cparser/GCC.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/cparser/GCC.mli b/cparser/GCC.mli
index 76f40372..f26d12df 100644
--- a/cparser/GCC.mli
+++ b/cparser/GCC.mli
@@ -13,6 +13,7 @@
(* *)
(* *********************************************************************)
-(* GCC built-ins *)
+(* GCC built-ins and attributes *)
val builtins: Builtins.t
+val attributes: (string * Cutil.attribute_class) list