diff options
| author | Hugo Herbelin | 2020-10-06 00:18:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:00:24 +0200 |
| commit | d98cca66ea0e64193e7f79ffcf99b632d0ad6f14 (patch) | |
| tree | 37d88269b02de930a3eb2dc62f6f1cbbcdb94942 /printing/ppconstr.mli | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Closes #13142 (more standardized pretty-printing of records).
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 |