diff options
| author | Brian Campbell | 2018-06-20 18:20:36 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-20 18:21:27 +0100 |
| commit | 18fea097306ac58732a0354ae6b0c00f9014975c (patch) | |
| tree | bb7431603486add51b1aada57197603902b83158 /src | |
| parent | 8450a064ab4c3c5a639e14001a971f2dc8fd148c (diff) | |
Coq: Generate MR when appropriate; syntax fixes
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index e9deaea2..09cbbecf 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -461,7 +461,10 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let doc_tannot_lem ctxt env eff typ = let of_typ typ = let ta = doc_typ ctxt typ in - if eff then string " : M " ^^ parens ta + if eff then + if ctxt.early_ret + then string " : MR " ^^ parens ta ^^ string " _" + else string " : M " ^^ parens ta else string " : " ^^ ta in if contains_t_pp_var ctxt typ @@ -1093,9 +1096,9 @@ let doc_exp_lem, doc_let_lem = separate space [string ">>= fun varstup => let"; doc_pat ctxt true (pat, typ_of e1); - string "= varstup in"] + string ":= varstup in"] | _ -> - separate space [string ">>= fun"; doc_pat ctxt true (pat, typ_of e1); bigarrow] + separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow] in infix 0 1 middle (expV b e1) (expN e2) in |