diff options
| -rw-r--r-- | plugins/extraction/extraction.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13581.v | 6 |
2 files changed, 11 insertions, 4 deletions
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. *) diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v new file mode 100644 index 0000000000..9f129f331e --- /dev/null +++ b/test-suite/bugs/closed/bug_13581.v @@ -0,0 +1,6 @@ +From Coq Require Extraction. + +Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }. +Definition d := Mixin nat tt (fun x => x). + +Extraction TestCompile d. |