diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index cce3c2d3..90484598 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1729,7 +1729,11 @@ let doc_exp, doc_let = if effectful eff then "autocast_m", "projT1_m" else "autocast", "projT1" in - let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in + (* We need to unpack an existential if it's generated by a pure + computation, or if the monadic binding isn't expecting one. *) + let epp = if unpack && not (effectful eff && packeff) + then string proj_id ^/^ parens epp + else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in let epp = if effectful eff && packeff && not unpack |