Changeset 2468 for src/common/Events.ma

Timestamp:

Nov 15, 2012, 6:12:57 PM (9 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:

• src/common/Events.ma (modified) (2 diffs)

src/common/Events.ma

@@ -38 +38 @@
 
 inductive eventval: Type[0] ≝
-  | EVint: ∀sz. bvint sz → eventval
-  | EVfloat: float → eventval.
+  | EVint: ∀sz. bvint sz → eventval.
+(*  | EVfloat: float → eventval.*)
 
 inductive event : Type[0] ≝
@@ -194 +194 @@
   | ev_match_int:
       ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
-  | ev_match_float:
-      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
+(*  | ev_match_float:
+      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f) *).
 
 inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=