diff options
Diffstat (limited to 'lib/coq/Sail2_values.v')
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 7c70f88b..55d85b3a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1032,6 +1032,7 @@ Arguments write_to [_ _ _]. Arguments of_regval [_ _ _]. Arguments regval_of [_ _ _]. +(* Register accessors: pair of functions for reading and writing register values *) Definition register_accessors regstate regval : Type := ((string -> regstate -> option regval) * (string -> regval -> regstate -> option regstate)). |