aboutsummaryrefslogtreecommitdiff
path: root/parsing/printer.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.mli')
-rw-r--r--parsing/printer.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 3a5c3decae..cdd2f42770 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -104,7 +104,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds
(** Proofs *)
val pr_goal : goal sigma -> std_ppcmds
-val pr_subgoals : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds
+val pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds
val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds
val pr_concl : int -> evar_map -> goal -> std_ppcmds
@@ -138,7 +138,7 @@ val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
type printer_pr = {
- pr_subgoals : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
pr_goal : goal sigma -> std_ppcmds;
};;