diff options
Diffstat (limited to 'parsing')
| -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 |