diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f25f63624..5aee70194 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 @@ -1066,8 +1066,10 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match cb.const_proj with - | None -> mk_typ (get_body c) - | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) + | false -> mk_typ (get_body c) + | true -> + let pb = lookup_projection (Projection.make kn false) env in + mk_typ (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1077,8 +1079,10 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_ax () | Def c -> (match cb.const_proj with - | None -> mk_def (get_body c) - | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) + | false -> mk_def (get_body c) + | true -> + let pb = lookup_projection (Projection.make kn false) env in + mk_def (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) |