Coq: add missing property derivation casts for effectful expressions

These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 3083fc29..1fea72ea 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1961,6 +1961,10 @@ let doc_exp, doc_let =
          if effects then
            match cast_ex, outer_ex with
            | ExGeneral, ExNone -> string "projT1_m" ^/^ parens epp
+           | ExGeneral, ExGeneral ->
+              if alpha_equivalent env cast_typ outer_typ
+              then epp
+              else string "derive_m" ^/^ parens epp
            | _ -> epp
          else match cast_ex with
               | ExGeneral -> string "projT1" ^/^ parens epp