diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 4 | ||||
| -rw-r--r-- | test/coq/pass/returnwithfact.sail | 19 |
2 files changed, 23 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 diff --git a/test/coq/pass/returnwithfact.sail b/test/coq/pass/returnwithfact.sail new file mode 100644 index 00000000..14179c17 --- /dev/null +++ b/test/coq/pass/returnwithfact.sail @@ -0,0 +1,19 @@ +default Order dec +$include <prelude.sail> + +val f : int -> range(2,6) effect {escape} + +val g1 : (bool,int) -> range(0,8) effect {escape} + +function g1(b,x) = { + if b then + return f(x) + else { + return f(x+1); + 5 + } +} + +val g2 : int -> range(0,8) effect {escape} + +function g2(x) = f(x) |