From 75b7729d204c7bae280d859bb233750f7c4b543e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 18 Feb 2018 19:08:04 +0100 Subject: Adding mention of shelved/given-up status in "Show Existentials". Also changed the API of pr_subgoals now using labels. Also removed a trailing space in printing existentials. --- printing/printer.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index a3427920a..9b26d4c84 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -181,8 +181,7 @@ val pr_goal : goal sigma -> Pp.t focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list - -> goal list -> goal list -> Pp.t +val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t @@ -190,7 +189,7 @@ val pr_concl : int -> evar_map -> goal -> Pp.t 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 -> int -> evar_info Evar.Map.t -> 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 : 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 @@ -223,7 +222,8 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } -- cgit v1.2.3