diff options
Diffstat (limited to 'printing/proof_diffs.mli')
| -rw-r--r-- | printing/proof_diffs.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 0d3b5821e5..482f03b686 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -30,6 +30,8 @@ val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t open Evd open Proof_type +open Environ +open Constr (** Computes the diff between two goals @@ -46,6 +48,10 @@ val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> 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 + (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) val log_out_ch : out_channel ref |