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

3 files changed, 3 insertions, 14 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index f3ef4dc76c..11d70529d7 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -38,7 +38,7 @@ GEXTEND Gram
     [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c
 (*VernacGoal c*)
 (*      | IDENT "Goal" -> VernacGoal None*)
-      | "Proof" -> VernacNop
+      | "Proof" -> VernacProof Tacexpr.TacId
       | "Proof"; "with"; ta = tactic -> VernacProof ta
 (* Used ?? 
       |	IDENT "Begin" -> VernacNop
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9d20226b7a..0cb0b54e12 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -593,7 +593,7 @@ let vernac_solve_existential = instantiate_nth_evar_com
 let vernac_set_end_tac tac =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode";
-  set_end_tac (Tacinterp.interp tac)
+  if tac <> Tacexpr.TacId then set_end_tac (Tacinterp.interp tac)
 
  
    
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 =