diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f25f6362..67c605ea 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -431,7 +431,7 @@ and extract_really_ind env kn mib = let packets = Array.mapi (fun i mip -> - let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let ar = EConstr.of_constr ar in let info = (fst (flag_of_type env sg ar) = Info) in @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if List.is_empty l then raise (I Standard); - if Option.is_empty mib.mind_record then raise (I Standard); + if mib.mind_record == Declarations.NotRecord then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with @@ -1065,9 +1065,14 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match cb.const_proj with + (match Recordops.find_primitive_projection kn with | None -> mk_typ (get_body c) - | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) + | Some p -> + let p = Projection.make p false in + let ind = Projection.inductive p in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(Projection.arg p) in + mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1076,9 +1081,14 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match cb.const_proj with + (match Recordops.find_primitive_projection kn with | None -> mk_def (get_body c) - | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) + | Some p -> + let p = Projection.make p false in + let ind = Projection.inductive p in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(Projection.arg p) in + mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) |