diff options
| author | Hugo Herbelin | 2019-11-18 16:04:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | 490704f4b2db98f4ef15f5e380b63e49e13a418b (patch) | |
| tree | 625e60c878e2768dbce36129e1df80ceace17495 /printing/proof_diffs.mli | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
Moving the diversity of constr printers to a label style.
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
Diffstat (limited to 'printing/proof_diffs.mli')
| -rw-r--r-- | printing/proof_diffs.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index a806ab7123..eebdaccd32 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -57,9 +57,9 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list -val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t -val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t -val pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t +val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t +val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t (** Computes diffs for a single conclusion *) val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t |