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
---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

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)
 
  
    
-- 
cgit v1.2.3