diff options
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 13e9be8e..cad35034 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -49,7 +49,7 @@ Require Import Kildall. Definition valnum := positive. -Inductive rhs : Set := +Inductive rhs : Type := | Op: operation -> list valnum -> rhs | Load: memory_chunk -> addressing -> list valnum -> rhs. @@ -85,7 +85,7 @@ Qed. we maintain the next unused value number, so as to easily generate fresh value numbers. *) -Record numbering : Set := mknumbering { +Record numbering : Type := mknumbering { num_next: valnum; num_eqs: list (valnum * rhs); num_reg: PTree.t valnum |