diff options
| author | Brian Campbell | 2019-03-05 12:13:53 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-05 12:13:53 +0000 |
| commit | 080205194a861882918e10de7680201c64f99142 (patch) | |
| tree | 4a4818a55985db6b5ed908c6708727c5443572ec /src | |
| parent | 361458ae5dbe8414b5a7ba1bc51ece8ebcfd5bc5 (diff) | |
Coq: output type-level Int definitions
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 42780012..734e3c02 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -2089,6 +2089,7 @@ let rec doc_range ctxt (BF_aux(r,_)) = match r with | BF_concat(ir1,ir2) -> (doc_range ctxt ir1) ^^ comma ^^ (doc_range ctxt ir2) *) +(* TODO: check use of empty_ctxt below *) let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with | TD_abbrev(id,typq,A_aux (A_typ typ, _)) -> let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in @@ -2097,6 +2098,14 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with doc_typquant_items empty_ctxt parens typq; colon; string "Type"]) (doc_typschm empty_ctxt false typschm) ^^ dot + | TD_abbrev(id,typq,A_aux (A_nexp nexp,_)) -> + let idpp = doc_id_type id in + doc_op coloneq + (separate space [string "Definition"; idpp; + doc_typquant_items empty_ctxt parens typq; + colon; string "Z"]) + (doc_nexp empty_ctxt nexp) ^^ dot ^^ hardline ^^ + separate space [string "Hint Unfold"; idpp; colon; string "sail."] | TD_abbrev _ -> empty (* TODO? *) | TD_bitfield _ -> empty (* TODO? *) | TD_record(id,typq,fs,_) -> |