diff options
| author | Pierre-Marie Pédrot | 2018-11-21 13:03:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-21 13:03:27 +0100 |
| commit | 4d0fea2ededb11d79f4f1abcc1595f9cec20d6dd (patch) | |
| tree | bbd47886f4649999ecad9f21ffb6ff55869f0132 /printing/proof_diffs.mli | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
| parent | 417641e48129c9ba8656c622c9b64cd32641e7de (diff) | |
Merge PR #8998: [legacy proof engine] Remove some cruft.
Diffstat (limited to 'printing/proof_diffs.mli')
| -rw-r--r-- | printing/proof_diffs.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 832393e15f..ce9ee5ae6f 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,7 +16,6 @@ val write_diffs_option : string -> unit val show_diffs : unit -> bool open Evd -open Proof_type open Environ open Constr @@ -31,7 +30,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 +42,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 +52,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 +60,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 *) |