Merge PR #8137: Fix 8132. Print the content of body, not its type.

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