From 82abccdc576e3eff3adb617e90fc9c4ececae329 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Mar 2015 13:38:58 +0100
Subject: Generalisation of the "end command" argument of the goal printer.

This is meant to help integrate the printers of the declarative mode.
---
 printing/printer.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 42ed2b6d9e..a469a8dbed 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -128,7 +128,7 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -168,7 +168,7 @@ val pr_assumptionset :
 val pr_goal_by_id : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
-- 
cgit v1.2.3