From 18c922c5e61bc7effb23da06c08bbf7b07baa344 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Dec 2003 17:00:42 +0000
Subject: Bug affichage Decompose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5144 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 f729ccd3cc..980bc63c23 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -517,7 +517,7 @@ and pr_atom1 = function
   | TacDecompose (l,c) ->
       hov 1 (str "Decompose" ++ spc () ++
         hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
-	  ++ str "]"))
+	  ++ str "]" ++ pr_arg pr_constr c))
   | TacSpecialize (n,c) ->
       hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c)
   | TacLApply c -> 
-- 
cgit v1.2.3