summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem_ast.ml
diff options
context:
space:
mode:
authorThomas Bauereiss2017-09-13 17:19:13 +0100
committerThomas Bauereiss2017-09-14 13:11:44 +0100
commit3914be09d200eb92ed1e317123f56667d597b5a7 (patch)
tree07ae483bb225f4e8290f77d236b0419b445f9c0c /src/pretty_print_lem_ast.ml
parentaa1f89abb2f42d085bd123147144c9c5c7ceb22f (diff)
Fix a regression when writing to a register via a reference in a vector such as GPR
This was wrongly translated as an update of the vector of references.
Diffstat (limited to 'src/pretty_print_lem_ast.ml')
-rw-r--r--src/pretty_print_lem_ast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 68745bf9..73f06d1a 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -210,7 +210,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
(match t with
| Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
| Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
- | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^
+ | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ " " ^
(pp_format_l_lem l) ^ ")"
and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
"(NC_aux " ^