From 153efd716c138af1f1a86df63e54b25bedaeb06c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 18 Jul 2007 15:20:49 +0000
Subject: 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
---
 parsing/printer.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/parsing/printer.ml b/parsing/printer.ml
index dc7552fcd1..52e5cb836c 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 =
-- 
cgit v1.2.3