diff options
| author | Shaked Flur | 2019-07-18 10:13:10 +0100 |
|---|---|---|
| committer | Shaked Flur | 2019-07-18 10:13:10 +0100 |
| commit | 1bb77b31f84946f036c0b7e37245809bbdb82def (patch) | |
| tree | 368af2665e2a213f3b374f41f5c6e93ecbf2d026 /src/pretty_print_lem.ml | |
| parent | 0a8981186d4da342ef36179cf093e64674573c63 (diff) | |
Support DMB/DSB domains
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 4890b8d1..2d8b282e 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1129,6 +1129,8 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -1201,6 +1203,8 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty |