diff options
Diffstat (limited to 'cparser/Cabs.v')
| -rw-r--r-- | cparser/Cabs.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 3255bc55..23c1cdc5 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -184,6 +184,7 @@ Definition name_group := (list spec_elem * list name)%type. *) Inductive definition := | FUNDEF : list spec_elem -> name -> statement -> cabsloc -> definition + | KRFUNDEF : list spec_elem -> name -> list string -> list definition -> statement -> cabsloc -> definition | DECDEF : init_name_group -> cabsloc -> definition (* global variable(s), or function prototype *) | PRAGMA : string -> cabsloc -> definition |