From ea1eaa9b152b73652f417e02bd469e5b289cec47 Mon Sep 17 00:00:00 2001
From: corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 26 Apr 2007 08:54:28 +0000
Subject: fin des conclusions multiples

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'ide/coqide.ml')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 25af11363..90130da37 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -804,17 +804,15 @@ object(self)
       proof_buffer#insert 
 	(Printf.sprintf "    *** Declarative Mode ***\n");
       try 
-	let (hyps,metas) = get_current_pm_goal () in
+	let (hyps,concl) = get_current_pm_goal () in
 	List.iter
 	  (fun ((_,_,_,(s,_)) as _hyp) -> 
 	     proof_buffer#insert (s^"\n"))
 	  hyps;
 	proof_buffer#insert 
 	  (String.make 38 '_' ^ "\n");
-	List.iter
-	  (fun (_,_,m) -> 
-	     proof_buffer#insert (m^"\n"))
-	  metas;
+	let (_,_,_,s) = concl in 
+	  proof_buffer#insert ("thesis := \n "^s^"\n");
 	let my_mark = `NAME "end_of_conclusion" in
 	  proof_buffer#move_mark
 	    ~where:((proof_buffer#get_iter_at_mark `INSERT)) 
-- 
cgit v1.2.3