diff options
| author | herbelin | 2000-12-14 22:13:07 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-14 22:13:07 +0000 |
| commit | 42679bb4f94de0a25d6fe5a959e00cfe7a1454d9 (patch) | |
| tree | 02bca1d940eb146b99298a5ed9182122f73160e0 /parsing/pretty.ml | |
| parent | 32db56471909ae183832989670a81bf59b8a8e5c (diff) | |
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
Diffstat (limited to 'parsing/pretty.ml')
| -rw-r--r-- | parsing/pretty.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |