From 42679bb4f94de0a25d6fe5a959e00cfe7a1454d9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Dec 2000 22:13:07 +0000
Subject: Les params d'inductif deviennent en même temps propre à chaque
 inductif d'un bloc et en même temps factorisés dans l'arité et les
 constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour
 mutual_inductive_body); accessoirement cela permet de factoriser le calcul
 des univers des paramètres dans safe_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'parsing/pretty.ml')

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index c22e869430..097a88e5a9 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -85,7 +85,9 @@ let print_mutual sp mib =
   let pk = kind_of_path sp in
   let env = Global.env () in
   let evd = Evd.empty in
-  let {mind_packets=mipv; mind_nparams=nparams} = mib in 
+  let {mind_packets=mipv} = mib in 
+  (* On suppose que tous les inductifs ont les même paramètres *)
+  let nparams = mipv.(0).mind_nparams in
   let (lpars,_) = decomp_n_prod env evd nparams
 		    (body_of_type (mind_user_arity mipv.(0))) in
   let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
-- 
cgit v1.2.3