diff options
| author | herbelin | 2003-12-24 17:00:42 +0000 |
|---|---|---|
| committer | herbelin | 2003-12-24 17:00:42 +0000 |
| commit | 18c922c5e61bc7effb23da06c08bbf7b07baa344 (patch) | |
| tree | 410f3fbd2153991cfac3f8efcb9c6db424dadccc | |
| parent | d51c877557b84551bee0b477629072b6b6995026 (diff) | |
Bug affichage Decompose
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5144 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |