diff options
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1320cce9b..158906dd2 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -17,14 +17,6 @@ open Names open Misctypes open Notation_term -val extract_lam_binders : - constr_expr -> local_binder_expr list * constr_expr -val extract_prod_binders : - constr_expr -> local_binder_expr list * constr_expr -val split_fix : - int -> constr_expr -> constr_expr -> - local_binder_expr list * constr_expr * constr_expr - val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t |