diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 05292b06b..bed7c39fe 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in - let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in + let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then @@ -174,10 +175,11 @@ let print_record env mind mib udecl = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in - let cstrtype = hnf_prod_applist env cstrtypes.(0) args in + let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) |