diff options
| author | Brian Campbell | 2019-03-12 12:43:50 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-12 12:43:50 +0000 |
| commit | b0e0902a82f61d53ad3778b2683215ad03d056b7 (patch) | |
| tree | 229ce6ee0d0287888494d6c9b50f3d628eb0752c /src | |
| parent | c3d10cdb1787077425e174fa638f1d43de7c797f (diff) | |
Coq: fix parametrized record types
Diffstat (limited to 'src')
| -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 f22ff758..d720312f 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -2138,10 +2138,11 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with string "Defined." ^^ hardline else empty in + let resetimplicit = separate space [string "Arguments"; id_pp; colon; string "clear implicits."] in doc_op coloneq - (separate space [string "Record"; id_pp; doc_typquant_items empty_ctxt parens typq]) + (separate space [string "Record"; id_pp; doc_typquant_items empty_ctxt braces typq]) ((*doc_typquant typq*) (braces (space ^^ align fs_doc ^^ space))) ^^ - dot ^^ hardline ^^ eq_pp ^^ updates_pp + dot ^^ hardline ^^ resetimplicit ^^ hardline ^^ eq_pp ^^ updates_pp | TD_variant(id,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty |