From c0fca6e10a2a1796035fdc2b6b2e344fecbe1233 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 13 Aug 2003 23:22:43 +0000
Subject: Hack pour ajouter Proof apres Correctness

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

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 8935b36b72..c0d57c5b6d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1050,6 +1050,7 @@ and pr_extend s cl =
             | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
         (str hd,cl) rl in
     hov 1 pp
+    ++ (if s = "Correctness" then sep_end () ++ fnl() ++ str "Proof" else mt())
   with Not_found ->
     hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
-- 
cgit v1.2.3