diff options
| author | Brian Campbell | 2018-05-29 15:43:39 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | 548d02f6667644154c5b5547331e34a278bae22c (patch) | |
| tree | 9b0e51103f50b2c25882b268f7cc0e6f8bb0d342 /src/pretty_print_coq.ml | |
| parent | 0f7f8d3ead1463b90353d00d0b48fdca151e8a84 (diff) | |
Coq: use record update syntax (only single fields work for now)
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 6821b92c..b0d7cb0e 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -57,7 +57,7 @@ fix_id doc_quant_item on constraints type quantifiers in records, unions - update notation for records + multiple update notation for records register_refs? should I control the nexps somewhat? L_real @@ -109,6 +109,7 @@ let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar let enclose_record = enclose (string "{| ") (string " |}") +let enclose_record_update = enclose (string "{[ ") (string " ]}") let bigarrow = string "=>" let separate_opt s f l = separate s (Util.map_filter f l) @@ -859,7 +860,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_record tid env -> tid | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in - anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = |