fin des conclusions multiples

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 7 insertions, 20 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 16b2460adf..930c50a77e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -269,24 +269,13 @@ let prepare_goal sigma g =
   (prepare_hyps sigma env,
    (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
 
-let prepare_meta sigma env (m,typ)  =
-  env, sigma, 
-  (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ))
-
-let prepare_metas info sigma env =
-  List.fold_right 
-    (fun cpl acc ->  
-      let meta = prepare_meta sigma env cpl in meta :: acc)
-    info.pm_subgoals [] 
-
 let get_current_pm_goal () =
   let pfts = get_pftreestate ()  in
   let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
-  let info = Decl_mode.get_info gls.it in
-  let env = pf_env gls in
   let sigma= sig_sig gls in
-    (prepare_hyps sigma env,
-     prepare_metas info sigma env)
+  let gl = sig_it gls in
+    prepare_goal sigma gl
+
 
 let get_current_goals () = 
     let pfts = get_pftreestate () in
diff --git a/ide/coq.mli b/ide/coq.mli
index 7b43a0c958..991f104dbe 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -33,7 +33,7 @@ type goal = hyp list * concl
 
 val get_current_goals : unit -> goal list
 
-val get_current_pm_goal : unit -> hyp list * meta list
+val get_current_pm_goal : unit -> goal
 
 val get_current_goals_nb : unit -> int
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 25af113639..90130da377 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))