diff options
| author | Thomas Bauereiss | 2017-10-19 15:39:43 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-10-19 16:00:55 +0100 |
| commit | 40a5395c1be351cb8abccb3ccc6fc4399d2d0e70 (patch) | |
| tree | 33a439d4bed42d707d6e3fa5042f637d7410d0a6 /src | |
| parent | faa725a8f0211ca7bc7aeb48f41dbf93380324ff (diff) | |
Fix pretty-printing of type abbreviation definitions with arguments
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index f135da4e..5d574638 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1093,9 +1093,10 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with - | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "type"; space; doc_id_lem_type id]) - (doc_typschm_lem sequential mwords false typschm) + | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) -> + doc_op equals + (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq]) + (doc_typschm_lem sequential mwords false typschm) | TD_record(id,nm,typq,fs,_) -> let fname fid = if prefix_recordtype then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] |