diff options
| author | Maxime Dénès | 2019-03-01 15:27:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-20 09:33:15 +0100 |
| commit | 27d453641446b3d35aa2211b94f949b57a88ebb2 (patch) | |
| tree | af47b4cb0e3fbb7fde26b6cab3a9b78b99699e94 /printing/ppconstr.mli | |
| parent | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (diff) | |
Stop accessing proof env via Pfedit in printers
This should make https://github.com/coq/coq/pull/9129 easier.
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1cb3aa6d7a..db1687a49b 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,19 +41,19 @@ val pr_guard_annot : (constr_expr -> Pp.t) -> Pp.t val pr_record_body : (qualid * constr_expr) list -> Pp.t -val pr_binders : local_binder_expr list -> Pp.t -val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t -val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t -val pr_constr_expr : constr_expr -> Pp.t -val pr_lconstr_expr : constr_expr -> 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 +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 : tolerability -> constr_expr -> Pp.t +val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t type term_pr = { - pr_constr_expr : constr_expr -> Pp.t; - pr_lconstr_expr : constr_expr -> Pp.t; - pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; - pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t + pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; + pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; + pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t } val set_term_pr : term_pr -> unit |