From e166e675f8623cc8405663e4cb03aa236e19ea3e Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 10 Oct 2003 19:00:57 +0000
Subject: show_subgoals dans Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4576 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/centaur.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 78de2fb02..10fcf37f2 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -586,7 +586,8 @@ open Vernacentries
 let pcoq_show_goal = function
   | Some n -> show_nth n
   | None ->
-      if !pcoq_started = Some true (* = debug *) then show_open_subgoals ()
+      if !pcoq_started = Some true (* = debug *) then
+	msg (Pfedit.pr_open_subgoals ())
       else errorlabstrm "show_goal"
 	(str "Show must be followed by an integer in Centaur mode");;
 
-- 
cgit v1.2.3