diff options
| author | Emilio Jesus Gallego Arias | 2018-11-16 20:16:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-21 01:26:45 +0100 |
| commit | 417641e48129c9ba8656c622c9b64cd32641e7de (patch) | |
| tree | bbd47886f4649999ecad9f21ffb6ff55869f0132 /printing/printer.mli | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
[legacy proof engine] Remove some cruft.
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 15 |
1 files changed, 7 insertions, 8 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 |