Current diff code only compares the first current goal of the old and new

proof states.  That's not always correct.  This change will a) show diffs
for all displayed goals and b) correctly match goals between the old and
new proof states.

For example, "split." will show diffs for both resulting goals.
"all: swap 1 2" will show the same diffs as for the old proof state, though
in a different position in the output.

Please see comments before Proof_diffs.make_goal_map_i and Proof_diffs.match_goals
for a description of how goals are matched between old and new proofs.

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