diff options
| -rw-r--r-- | parsing/prettyp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 41a4a6b5a4..867bcd3168 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -107,9 +107,11 @@ let build_inductive sp tyi = let (mib,mip) = Global.lookup_inductive (sp,tyi) in let params = mip.mind_params_ctxt in let args = extended_rel_list 0 params in - let indf = make_ind_family ((sp,tyi),args) in - let arity = mip.mind_user_arity in - let cstrtypes = arities_of_constructors (Global.env()) (sp,tyi) in + let env = Global.env() in + let arity = hnf_prod_applist env mip.mind_user_arity args in + let cstrtypes = arities_of_constructors env (sp,tyi) in + let cstrtypes = + Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let cstrnames = mip.mind_consnames in (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes) |