diff options
author | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-26 08:54:28 +0000 |
---|---|---|
committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-26 08:54:28 +0000 |
commit | ea1eaa9b152b73652f417e02bd469e5b289cec47 (patch) | |
tree | 4d654ad1434bac0781eb4f3e6f1505c3895df4ba /ide/coqide.ml | |
parent | 40425048feff138e6c67555c7ee94142452d1cae (diff) |
fin des conclusions multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r-- | ide/coqide.ml | 8 |
1 files changed, 3 insertions, 5 deletions
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)) |