From 908a2269893046eada0e51a88aa7fdd5ced227ea Mon Sep 17 00:00:00 2001
From: jforest
Date: Tue, 22 Aug 2006 09:43:51 +0000
Subject: making otags working

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 8e7af67b0c..b3a8abce55 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -820,7 +820,7 @@ let rec pr_vernac = function
 
   (* For extension *)
   | VernacExtend (s,c) -> pr_extend s c
-  | VernacProof Tacexpr.TacId _ -> str "Proof"
+  | VernacProof (Tacexpr.TacId _) -> str "Proof"
   | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
 
 and pr_extend s cl =
-- 
cgit v1.2.3