Merge PR #8247: Show diffs on multiple changed goals; match old and new goal info

1 files changed, 20 insertions, 9 deletions

diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 482f03b686..832393e15f 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -15,8 +15,13 @@ val write_diffs_option : string -> unit
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
-(** Computes the diff between the first goal of two Proofs and returns
-the highlighted hypotheses and conclusion.
+open Evd
+open Proof_type
+open Environ
+open Constr
+
+(** Computes the diff between the goals of two Proofs and returns
+the highlighted lists of hypotheses and conclusions.
 
 If the strings used to display the goal are not lexable (this is believed
 unlikely), this routine will generate a Diff_Failure.  This routine may also
@@ -26,12 +31,7 @@ If you want to make your call especially bulletproof, catch these
 exceptions, print a user-visible message, then recall this routine with
 the first argument set to None, which will skip the diff.
 *)
-val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t
-
-open Evd
-open Proof_type
-open Environ
-open Constr
+val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t
 
 (** Computes the diff between two goals
 
@@ -43,7 +43,7 @@ If you want to make your call especially bulletproof, catch these
 exceptions, print a user-visible message, then recall this routine with
 the first argument set to None, which will skip the diff.
 *)
-val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t
+val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t
 
 (** Convert a string to a list of token strings using the lexer *)
 val tokenize_string : string -> string list
@@ -52,6 +52,17 @@ val pr_letype_core         : bool -> Environ.env -> Evd.evar_map -> EConstr.type
 val pr_leconstr_core       : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
 val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
 
+(** Computes diffs for a single conclusion *)
+val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
+
+(** Generates a map from [np] to [op] that maps changed goals to their prior
+forms.  The map doesn't include entries for unchanged goals; unchanged goals
+will have the same goal id in both versions.
+
+[op] and [np] must be from the same proof document and [op] must be for a state
+before [np]. *)
+val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t
+
 (* Exposed for unit test, don't use these otherwise *)
 (* output channel for the test log file *)
 val log_out_ch : out_channel ref