diff options
| author | corbinea | 2007-04-26 08:54:28 +0000 |
|---|---|---|
| committer | corbinea | 2007-04-26 08:54:28 +0000 |
| commit | ea1eaa9b152b73652f417e02bd469e5b289cec47 (patch) | |
| tree | 4d654ad1434bac0781eb4f3e6f1505c3895df4ba /parsing/printer.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 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index c1a4415e32..7272ee697f 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -262,16 +262,15 @@ let default_pr_goal g = pr_context_of env, pr_ltype_env_at_top env g.evar_concl else - let {pm_subgoals=metas} = get_info g in - (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), + (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), pr_context_of env, - pr_subgoal_metas metas env + pr_ltype_env_at_top env g.evar_concl in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () + str"thesis := " ++ fnl () ++ str " " ++ pc) ++ fnl () (* display the conclusion of a goal *) let pr_concl n g = |