diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 13:07:53 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 13:07:53 +0100 |
commit | 284869d016607fad339ea4d06bf1433c6ec23672 (patch) | |
tree | 1cae1f278186bb0aa9643fb57ca9af0eb029672f /printing | |
parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
parent | 42610a4659cf35e6a005d79eec273c606bdf87dd (diff) |
Merge PR #1082: Fixing Print for inductive types with let-in in parameters
Diffstat (limited to 'printing')
-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 35487e09c..2cdb9be3f 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 @@ -173,10 +174,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)) |