diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/printer.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index dc7552fcd..52e5cb836 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -254,21 +254,22 @@ let pr_subgoal_metas metas env= (* display complete goal *) let default_pr_goal g = let env = evar_env g in - let preamb,penv,pc = + let preamb,thesis,penv,pc = if g.evar_extra = None then - mt (), + mt (), mt (), pr_context_of env, pr_ltype_env_at_top env g.evar_concl else (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), - pr_context_of env, - pr_ltype_env_at_top env g.evar_concl + (str"thesis := " ++ fnl ()), + pr_context_of 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"thesis := " ++ fnl () ++ str " " ++ pc) ++ fnl () + thesis ++ str " " ++ pc) ++ fnl () (* display the conclusion of a goal *) let pr_concl n g = |