diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0cad192332..30f90dd1fc 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -22,7 +22,6 @@ open Reductionops open Inductive open Termops open Inductiveops -open Recordops open Namegen open Miniml open Table @@ -428,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 @@ -463,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. *) @@ -531,7 +531,7 @@ and extract_really_ind env kn mib = let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in - List.iter (Option.iter check_proj) (lookup_projections ip) + List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip) with Not_found -> () end; Record field_glob @@ -1129,7 +1129,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_typ (get_body c) | Some p -> let body = fake_match_projection env p in @@ -1142,7 +1142,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_def (get_body c) | Some p -> let body = fake_match_projection env p in |