diff options
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index db1687a49b..2e00b12899 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -37,7 +37,7 @@ val pr_glob_level : Glob_term.glob_level -> Pp.t val pr_glob_sort : Glob_term.glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> - lident option * recursion_order_expr -> + recursion_order_expr CAst.t option -> Pp.t val pr_record_body : (qualid * constr_expr) list -> Pp.t |