summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-23 21:16:53 +0000
committerAlasdair Armstrong2018-01-23 21:16:53 +0000
commitdfa7d1d79631ce26ce6be98ddcf9a8c8e5d171f8 (patch)
tree88451ed7d2e51bba0c3814c4ef712eb5bd4a2638 /src/pretty_print_lem.ml
parentd94404854c10960c881b5146f81d4483e73a8ca6 (diff)
parent4ec26c81830b26957dfac205eb60b522890fb007 (diff)
Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a759162e..edddcdd3 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -721,7 +721,9 @@ let doc_exp_lem, doc_let_lem =
| E_field((E_aux(_,(l,fannot)) as fexp),id) ->
let ft = typ_of_annot (l,fannot) in
(match fannot with
- | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env ->
+ | Some(env, (Typ_aux (Typ_id tid, _)), _)
+ | Some(env, (Typ_aux (Typ_app (tid, _), _)), _)
+ when Env.is_record tid env ->
let fname =
if prefix_recordtype
then (string (string_of_id tid ^ "_")) ^^ doc_id_lem id