diff options
Diffstat (limited to 'cfrontend/Cminorgen.v')
| -rw-r--r-- | cfrontend/Cminorgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index cc5e5ab3..1045d1a0 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -108,7 +108,7 @@ Definition make_globaladdr (id: ident): expr := data block. [Var_global_scalar] and [Var_global_array] denote global variables, stored in the global symbols with the same names. *) -Inductive var_info: Set := +Inductive var_info: Type := | Var_local: memory_chunk -> var_info | Var_stack_scalar: memory_chunk -> Z -> var_info | Var_stack_array: Z -> var_info |