diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-11-13 15:20:12 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-11-13 15:20:12 +0100 |
| commit | 3f24b362f5ac2aa252ee14f1b793ebbf2f69ff08 (patch) | |
| tree | fe290a38c7675f965d0ffb67cde20d161ce4444e /cparser/Cabs.v | |
| parent | 4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4 (diff) | |
| parent | d90ba4443294b80bd940daedfdcdc3d4334fdc7c (diff) | |
| download | compcert-3f24b362f5ac2aa252ee14f1b793ebbf2f69ff08.tar.gz compcert-3f24b362f5ac2aa252ee14f1b793ebbf2f69ff08.zip | |
Merge branch 'master' of ssh://github.com/AbsInt/CompCert
Diffstat (limited to 'cparser/Cabs.v')
| -rw-r--r-- | cparser/Cabs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/Cabs.v b/cparser/Cabs.v index e15f8694..f5cab15a 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -81,6 +81,7 @@ with decl_type := | PTR : list cvspec -> decl_type -> decl_type (* The bool is true for variable length parameters. *) | PROTO : decl_type -> list parameter * bool -> decl_type + | PROTO_OLD : decl_type -> list string -> decl_type with parameter := | PARAM : list spec_elem -> option string -> decl_type -> list attribute -> cabsloc -> parameter @@ -190,8 +191,7 @@ Definition asm_flag := (bool * list char_code)%type. ** Declaration definition (at toplevel) *) Inductive definition := - | FUNDEF : list spec_elem -> name -> statement -> cabsloc -> definition - | KRFUNDEF : list spec_elem -> name -> list string -> list definition -> statement -> cabsloc -> definition + | FUNDEF : list spec_elem -> name -> list definition -> statement -> cabsloc -> definition | DECDEF : init_name_group -> cabsloc -> definition (* global variable(s), or function prototype *) | PRAGMA : string -> cabsloc -> definition |