diff options
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 |