From a265c1ad912b4940861ec27efd09e5b20d33233c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 6 Dec 2020 03:03:12 +0100 Subject: Fixing #13581: missing support for let-ins in arity of inductive types. At first view, the fix takes care about when to use the number of assumptions and when to also include local definitions, but I don't know all the details of the implementation to be absolutely sure. --- plugins/extraction/extraction.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ca4f5429a2..30f90dd1fc 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -427,6 +427,7 @@ and extract_really_ind env kn mib = (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in + let ndecls = List.length mib.mind_params_ctxt in let npar = mib.mind_nparams in let epar = push_rel_context mib.mind_params_ctxt env in let sg = Evd.from_env env in @@ -462,17 +463,17 @@ and extract_really_ind env kn mib = if not p.ip_logical then let types = arities_of_constructors env ((kn,i),u) in for j = 0 to Array.length types - 1 do - let t = snd (decompose_prod_n npar types.(j)) in + let t = snd (decompose_prod_n_assum ndecls types.(j)) in let prods,head = dest_prod epar t in let nprods = List.length prods in let args = match Constr.kind head with | App (f,args) -> args (* [Constr.kind f = Ind ip] *) | _ -> [||] in - let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in - let db = db_from_ind dbmap npar in + let dbmap = parse_ind_args p.ip_sign args (nprods + ndecls) in + let db = db_from_ind dbmap ndecls in p.ip_types.(j) <- - extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1) + extract_type_cons epar sg db dbmap (EConstr.of_constr t) (ndecls+1) done done; (* Third pass: we determine special cases. *) -- cgit v1.2.3