From 2425dd9e258fe67e01bc63b0c2e82db0ecc3cdd6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 7 Oct 2003 20:52:57 +0000
Subject: Debranchement de l'affichage automatique de Proof par le traducteur
 (trop complique de trouver la bonne indentation); affichage en revanche de
 Proof s'il existait deja

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4536 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppvernacnew.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

(limited to 'translate')

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 59df9d4d35..50de4ec320 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -63,14 +63,6 @@ let pr_reference r =
 
 let sep_end () = str"."
 
-let start_theorem = ref false
-
-let insert_proof_keyword () =
-  if !start_theorem then 
-    (start_theorem := false; hv 0 (str "Proof" ++ sep_end () ++ fnl()))
-  else
-    mt ()
-
 (* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *)
 (*
 let pr_raw_tactic_env l env t = 
@@ -634,7 +626,6 @@ let rec pr_vernac = function
         | Some cc -> str" :=" ++ spc() ++ cc))
 
   | VernacStartTheoremProof (ki,id,(bl,c),b,d) ->
-      start_theorem := true;
       hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++
       (match bl with
         | [] -> mt()
@@ -649,7 +640,6 @@ pr_vbinders bl ++ spc())
       |	None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_id id
       |	Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_id id)) 
   | VernacExactProof c ->
-      start_theorem := false;
       hov 2 (str"Proof" ++ pr_lconstrarg c)
   | VernacAssumption (stre,l) ->
       hov 2
@@ -906,13 +896,11 @@ pr_vbinders bl ++ spc())
 
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
-      insert_proof_keyword () ++
       (if i = 1 then mt() else int i ++ str ": ") ++
 (*      str "By " ++*)
       (if deftac then mt() else str "!! ") ++
       Options.with_option Options.translate_syntax (pr_raw_tactic_goal i) tac
   | VernacSolveExistential (i,c) ->
-      insert_proof_keyword () ++
       str"Existential " ++ int i ++ pr_lconstrarg c
 
   (* Auxiliary file and library management *)
@@ -1074,6 +1062,7 @@ pr_vbinders bl ++ spc())
   | VernacExtend (s,c) -> pr_extend s c
   | VernacV7only _ -> mt()
   | VernacV8only com -> pr_vernac com
+  | VernacProof Tacexpr.TacId -> str "Proof"
   | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
 
 and pr_extend s cl =
-- 
cgit v1.2.3