From 0c5ff0aa6cd611ab40233b284b0a6054bc27166e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 17 Jul 2018 16:06:27 +0100
Subject: Coq: support effectful function signatures in axiom generation

---
 src/pretty_print_coq.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/pretty_print_coq.ml')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 44670277..74e97a29 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1846,6 +1846,11 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
      let arg_typs_pp = separate space (List.map doc_typ' typs) in
      let _, ret_ty = replace_atom_return_type ret_ty in
      let ret_typ_pp = doc_typ empty_ctxt ret_ty in
+     let ret_typ_pp =
+       if effectful eff
+       then string "M" ^^ space ^^ parens ret_typ_pp
+       else ret_typ_pp
+     in
      let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in
      string "forall" ^/^ separate space tyvars_pp ^/^
        arg_typs_pp ^/^ separate space constrs_pp ^^ comma ^/^ ret_typ_pp
-- 
cgit v1.2.3