From f6558c8600a9a4c110141655cc3e414290b4bc22 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 1 Dec 2003 11:45:28 +0000
Subject: Bug traduction clearbody

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

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index bad3ac90f2..327ec7d08b 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -568,7 +568,7 @@ and pr_atom1 env = 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