diff options
Diffstat (limited to 'common/Values.v')
| -rw-r--r-- | common/Values.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/common/Values.v b/common/Values.v index 8182d7a..9645e8a 100644 --- a/common/Values.v +++ b/common/Values.v @@ -21,7 +21,7 @@ Require Import AST. Require Import Integers. Require Import Floats. -Definition block : Set := Z. +Definition block : Type := Z. Definition eq_block := zeq. (** A value is either: @@ -33,7 +33,7 @@ Definition eq_block := zeq. value of an uninitialized variable. *) -Inductive val: Set := +Inductive val: Type := | Vundef: val | Vint: int -> val | Vfloat: float -> val |