diff options
| author | Emilio Jesus Gallego Arias | 2020-02-22 13:51:55 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-22 13:51:55 -0500 |
| commit | fd67afe0f7c55799ae0a14d78f1007a0360bd552 (patch) | |
| tree | 7b77866dfda1c468eb3a0ddddd1afcd22af1a834 /printing/ppconstr.mli | |
| parent | 7ef010c50c9d8efcd20d44807126efcd418c4e0d (diff) | |
| parent | 2e64c61cf64172fb0dce2d8b3996fb30e179e5ea (diff) | |
Merge PR #11635: Cleanup around the tolerability structure
Reviewed-by: ejgallego
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index c17ca251a8..288fb251c4 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -15,9 +15,8 @@ open Libnames open Constrexpr open Names -open Notation_gram -val prec_less : precedence -> tolerability -> bool +val prec_less : entry_level -> entry_relative_level -> bool val pr_tight_coma : unit -> Pp.t @@ -49,7 +48,7 @@ val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t -val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t +val pr_constr_expr_n : Environ.env -> Evd.evar_map -> entry_relative_level -> constr_expr -> Pp.t type term_pr = { pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; @@ -76,8 +75,8 @@ val default_term_pr : term_pr Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) -val lsimpleconstr : tolerability -val ltop : tolerability +val lsimpleconstr : entry_relative_level +val ltop : entry_relative_level val modular_constr_pr : - ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) -> - (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t + ((unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t |