From 29a6b8ed0221b58813b26028ad990a6d7d340dbc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 27 May 2004 12:24:21 +0000
Subject: Bug affichage ClearBody

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

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fc44758bef..cd31b7f264 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -549,7 +549,7 @@ and pr_atom1 = function
   | TacClear l ->
       hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacClearBody l ->
-      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
+      hov 1 (str "ClearBody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->
       (* Rem: only b = true is available for users *)
       assert b;
-- 
cgit v1.2.3