Merge PR #8998: [legacy proof engine] Remove some cruft.

2 files changed, 11 insertions, 13 deletions

diff --git a/printing/printer.mli b/printing/printer.mli
index 785f452a7b..cefc005c74 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -13,7 +13,6 @@ open Constr
 open Environ
 open Pattern
 open Evd
-open Proof_type
 open Glob_term
 open Ltac_pretype
 
@@ -144,7 +143,7 @@ val pr_transparent_state   : TransparentState.t -> Pp.t
     records containing the goal and sigma for, respectively, the new and old proof steps,
     e.g. [{ it = g ; sigma = sigma }].
 *)
-val pr_goal                : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t
+val pr_goal                : ?diffs:bool -> ?og_s:(Goal.goal sigma) -> Goal.goal sigma -> Pp.t
 
 (** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals]
    prints the goals in [goals] followed by the goals in [unfocused] in a compact form
@@ -161,17 +160,17 @@ val pr_goal                : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma ->
    there are non-instantiated existential variables.  [stack] is used to print summary info on unfocused
    goals.
 *)
-val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map
-                             -> seeds:goal list -> shelf:goal list -> stack:int list
-                             -> unfocused: goal list -> goals:goal list -> Pp.t
+val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map
+                             -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list
+                             -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t
 
-val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
+val pr_subgoal             : int -> evar_map -> Goal.goal list -> Pp.t
 
 (** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma].  The output
     is labelled "subgoal [n]".  If [diffs] is true, highlight the differences between the old conclusion,
     [og_s], and [g]+[sigma].  [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }].
 *)
-val pr_concl               : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t
+val pr_concl               : int -> ?diffs:bool -> ?og_s:(Goal.goal sigma) -> evar_map -> Goal.goal -> Pp.t
 
 (** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop.
     The first active goal is printed with all its antecedents and the conclusion.  The other active goals only show their
@@ -182,7 +181,7 @@ val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
-val pr_evars_int           : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars_int           : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
 val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
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 *)