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
---
 parsing/g_proofs.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

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