diff options
Diffstat (limited to 'printing/proof_diffs.mli')
| -rw-r--r-- | printing/proof_diffs.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 832393e15f..1ebde3d572 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -12,11 +12,11 @@ (** Controls whether to show diffs. Takes values "on", "off", "removed" *) val write_diffs_option : string -> unit + (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool open Evd -open Proof_type open Environ open Constr @@ -31,7 +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_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t +val diff_goal_ide : Goal.goal sigma option -> Goal.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_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t +val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list @@ -53,7 +53,7 @@ val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.cons 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 +val diff_concl : ?og_s:Goal.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 @@ -61,7 +61,7 @@ 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 +val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) |