diff options
| author | Thomas Bauereiss | 2018-01-23 19:51:39 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-01-23 19:53:17 +0000 |
| commit | 4ec26c81830b26957dfac205eb60b522890fb007 (patch) | |
| tree | bb862e4d9a08999ff96e360803e3630a5964624c /src/pretty_print_lem.ml | |
| parent | c5db705ca228421b4035b4361aba9823750fd67c (diff) | |
Run tests for Lem shallow embedding
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer
and rewriter uncovered by the tests.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
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 |