diff options
| author | coqbot-app[bot] | 2020-10-15 11:13:43 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-15 11:13:43 +0000 |
| commit | 56384cc09d6d9e9446e7c11aee5def865e28a4d5 (patch) | |
| tree | 46a673c5b4601f8d1fb93421945b504642b9a6bb /printing/ppconstr.mli | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
| parent | d98cca66ea0e64193e7f79ffcf99b632d0ad6f14 (diff) | |
Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq records
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 2850e4bfa0..02e04573f8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,7 +41,8 @@ val pr_guard_annot -> recursion_order_expr option -> Pp.t -val pr_record_body : (qualid * constr_expr) list -> Pp.t +val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t +val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t |