Closed rudynicolop closed 2 years ago
Cleaner lvalues.
ValueLvalue
Inductive
tags_t
ValLeftName
exec_read_array_access
Interpreter.v
The build seems to work on my machine.
Cleaner lvalues.
ValueLvalueis no longer a mutuallyInductivedata type.ValueLvalueno longer has type annotations & thus no longer depends ontags_t.ValLeftNameonly has a locator now.exec_read_array_accessuses the first header as the default value instead of generating one from a type annotation.Interpreter.v.The build seems to work on my machine.