From 2a805fd99b96746dbfe381d64cd7eaba84fdca79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jul 2014 15:59:44 +0200
Subject: Feedback: LoadedFile + Goals

LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
---
 printing/printer.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index eb181d4265..aa949232ac 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -128,7 +128,7 @@ val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
-val pr_open_subgoals       : unit -> std_ppcmds
+val pr_open_subgoals       : ?proof:Proof.proof -> unit -> std_ppcmds
 val pr_nth_open_subgoal    : int -> std_ppcmds
 val pr_evar                : (evar * evar_info) -> std_ppcmds
 val pr_evars_int           : int -> evar_info Evar.Map.t -> std_ppcmds
-- 
cgit v1.2.3