diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-18 15:20:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-18 15:20:49 +0000 |
| commit | 153efd716c138af1f1a86df63e54b25bedaeb06c (patch) | |
| tree | 33b5e598a3c6c4ed44cea6a69622aab99bb6a1b6 /parsing | |
| parent | f0127d555ca0143323854c48587e3b05fb370f9d (diff) | |
Affichage de "thesis" seulement en mode déclaratif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10024 85f007b7-540e-0410-9357-904b9bb8a0f7
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 = |