diff options
| author | Thomas Bauereiss | 2017-08-09 12:19:56 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-08-09 12:19:56 +0100 |
| commit | af1803ece80f4e278d2ff996bf9430a6a8551164 (patch) | |
| tree | 33d675cd54b043cffa9f96200f6d9422c4144e4f /src | |
| parent | 6100aecd642766252b73d3271a026d17de605fa0 (diff) | |
Pretty-print some more type annotations
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 955a148c..5fe6b69d 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -505,7 +505,8 @@ let doc_exp_lem, doc_let_lem = let (taepp,aexp_needed) = let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in let eff = effect_of full_exp in - if contains_bitvector_typ t && not (contains_t_pp_var t) + if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t) && + not (contains_t_pp_var t) then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true) else (epp, aexp_needed) in if aexp_needed then parens (align taepp) else taepp |