diff options
Diffstat (limited to 'printing/proof_diffs.mli')
| -rw-r--r-- | printing/proof_diffs.mli | 29 |
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 |