summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
authorThomas Bauereiss2017-07-26 12:03:12 +0100
committerThomas Bauereiss2017-07-26 12:03:12 +0100
commit26e59493cde0ffbf1868426fe3bec158f2dbaad0 (patch)
tree2193492e4989608eb5d2fef9ed3a60aa84b9c316 /src/pretty_print_lem.ml
parenteae4d12ad793809482252be0b459bb7e634b5482 (diff)
Improve rewriting of sizeof expressions
If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 9f479cdc..95ddc580 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -274,7 +274,7 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w
| Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
| _ -> doc_id_lem id end
| P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id])
- | P_typ(typ,p) -> doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ)
+ | P_typ(typ,p) -> parens (doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ))
| P_vector pats ->
let ppp =
(separate space)