Changeset 961 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (9 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r886 r961  
    2727| St_exit : nat → stmt
    2828(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    29 | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
     29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    3030| St_return : option (Σt. expr t) → stmt
    3131| St_label : ident → stmt → stmt
Note: See TracChangeset for help on using the changeset viewer.