Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9918 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 9 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 4619e50ec7..dc7552fcd1 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -171,15 +171,7 @@ let pr_named_context env ne_context =
           ne_context ~init:(mt ()))
 
 let pr_rel_context env rel_context =
-  let rec prec env = function
-    | [] -> (mt ()) 
-    | [b] -> str "(" ++ pr_rel_decl env b ++ str")"
-    | b::rest ->
-        let pb = pr_rel_decl env b in
-        let penvtl = prec (push_rel b env) rest in
-        str "(" ++ pb ++ str")" ++ spc () ++ penvtl
-  in 
-  hov 0 (prec env (List.rev rel_context))
+  pr_binders (extern_rel_context None env rel_context)
 
 let pr_rel_context_of env =
   pr_rel_context env (rel_context env)