From 5a44ea111daaddd4a0eae40068fb6d7ab2e351a9 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 27 Nov 2003 15:32:01 +0000
Subject: Hint Destruct mal affiche

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

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 87f4a7b5f5..4d78ee179a 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -221,7 +221,7 @@ let pr_hints local db h pr_c pr_pat =
     | HintsDestruct(name,i,loc,c,tac) ->
         str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++
         hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++
-               pr_c c ++ str " :=") ++ spc() ++
+               pr_c c ++ str " =>") ++ spc() ++
         pr_raw_tactic tac in
   hov 2 (str"Hint "++pr_locality local ++ pph ++ opth)
 
-- 
cgit v1.2.3