summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJon French2019-05-13 15:56:44 +0100
committerJon French2019-05-13 16:03:50 +0100
commit02fa50e64f79309f5a3da78737070dd9f8b3dce2 (patch)
tree577066e1eda94e080bd546d649e77d2ddcc3eb4a
parentca7812d3eb81f2ed7ce2884dafcf57a9da6a36b9 (diff)
don't emit cache_op_kind enum in Lem
-rw-r--r--src/pretty_print_lem.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 10441ed5..f13b8e1b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1193,6 +1193,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
| Id_aux ((Id "barrier_kind"),_) -> empty
| Id_aux ((Id "trans_kind"),_) -> empty
| Id_aux ((Id "instruction_kind"),_) -> empty
+ | Id_aux ((Id "cache_op_kind"),_) -> empty
| Id_aux ((Id "regfp"),_) -> empty
| Id_aux ((Id "niafp"),_) -> empty
| Id_aux ((Id "diafp"),_) -> empty