Changeset 2468 for src/common/AST.ma


Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (8 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r2439 r2468  
    128128inductive typ : Type[0] ≝
    129129  | ASTint : intsize → signedness → typ
    130   | ASTptr : (*region →*) typ
    131   | ASTfloat : floatsize → typ.
     130  | ASTptr : (*region →*) typ.
     131(*  | ASTfloat : floatsize → typ. *)
    132132
    133133(* XXX aliases *)
     
    246246  match ty with
    247247  [ ASTint sz _ ⇒ size_intsize sz
    248   | ASTptr  ⇒ size_pointer
    249   | ASTfloat sz ⇒ size_floatsize sz ].
     248  | ASTptr  ⇒ size_pointer ].
     249(*  | ASTfloat sz ⇒ size_floatsize sz ].*)
    250250
    251251lemma typesize_pos: ∀ty. typesize ty > 0.
Note: See TracChangeset for help on using the changeset viewer.