diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index dcba00196be30..08a1aa69b9789 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -244,6 +244,69 @@ let parse_ind_args si args relmax =
          | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
+(** Because of automatic unboxing the easy way [mk_def c] on the
+   constant body of primitive projections doesn't work. We pretend
+   that they are implemented by matches until someone figures out how
+   to clean it up (test with #4710 when working on this). *)
+let fake_match_projection env p =
+  let ind = Projection.Repr.inductive p in
+  let proj_arg = Projection.Repr.arg p in
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+  let indu = mkIndU (ind,u) in
+  let ctx, paramslet =
+    let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
+    let (ctx, cty) = mip.mind_nf_lc.(0) in
+    let cty = Term.it_mkProd_or_LetIn cty ctx in
+    let rctx, _ = decompose_prod_decls (Vars.substl subst cty) in
+    List.chop mip.mind_consnrealdecls.(0) rctx
+  in
+  let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+  let ci = {
+    ci_ind = ind;
+    ci_npar = mib.mind_nparams;
+    ci_cstr_ndecls = mip.mind_consnrealdecls;
+    ci_cstr_nargs = mip.mind_consnrealargs;
+    ci_relevance = Declareops.relevance_of_projection_repr mib p;
+    ci_pp_info;
+  }
+  in
+  let x = match mib.mind_record with
+    | NotRecord | FakeRecord -> assert false
+    | PrimRecord info ->
+      let x, _, _, _ = info.(snd ind) in
+      make_annot (Name x) mip.mind_relevance
+  in
+  let indty = mkApp (indu, Context.Rel.instance mkRel 0 paramslet) in
+  let rec fold arg j subst = function
+    | [] -> assert false
+    | LocalAssum (na,ty) :: rem ->
+      let ty = Vars.substl subst (liftn 1 j ty) in
+      if arg != proj_arg then
+        let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in
+        let proj_relevant = match na.binder_relevance with
+        | Sorts.Irrelevant -> false
+        | Sorts.Relevant -> true
+        | Sorts.RelevanceVar _ -> assert false
+        in
+        let kn = Projection.Repr.make ind ~proj_relevant ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
+        fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
+      else
+        let p = ([|x|], liftn 1 2 ty) in
+        let branch =
+          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
+          (nas, mkRel (List.length ctx - (j - 1)))
+        in
+        let params = Context.Rel.instance mkRel 1 paramslet in
+        let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
+        it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
+    | LocalDef (_,c,t) :: rem ->
+      let c = liftn 1 j c in
+      let c1 = Vars.substl subst c in
+      fold arg (j+1) (c1::subst) rem
+  in
+  fold 0 1 [] (List.rev ctx)
+
 (*S Extraction of a type. *)
 
 (* [extract_type env db c args] is used to produce an ML type from the
@@ -652,8 +715,13 @@ let rec extract_term env sg mle mlt c args =
     | Construct (cp,_) ->
         extract_cons_app env sg mle mlt cp args
     | Proj (p, c) ->
-        let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
-        extract_term env sg mle mlt term args
+        let p = Projection.repr p in
+        let term = fake_match_projection env p in
+        let ind = Inductiveops.find_rectype env sg (Retyping.get_type_of env sg c) in
+        let indf,_ = Inductiveops.dest_ind_type ind in
+        let _,indargs = Inductiveops.dest_ind_family indf in
+        let indargs = List.map EConstr.of_constr indargs in
+        extract_term env sg mle mlt (EConstr.of_constr term) (indargs@c::args)
     | Rel n ->
         (* As soon as the expected [mlt] for the head is known, *)
         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
@@ -1024,69 +1092,6 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
   current_fixpoints := [];
   Dfix (Array.map (fun kn -> GlobRef.ConstRef kn) vkn, terms, types)
 
-(** Because of automatic unboxing the easy way [mk_def c] on the
-   constant body of primitive projections doesn't work. We pretend
-   that they are implemented by matches until someone figures out how
-   to clean it up (test with #4710 when working on this). *)
-let fake_match_projection env p =
-  let ind = Projection.Repr.inductive p in
-  let proj_arg = Projection.Repr.arg p in
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-  let indu = mkIndU (ind,u) in
-  let ctx, paramslet =
-    let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
-    let (ctx, cty) = mip.mind_nf_lc.(0) in
-    let cty = Term.it_mkProd_or_LetIn cty ctx in
-    let rctx, _ = decompose_prod_decls (Vars.substl subst cty) in
-    List.chop mip.mind_consnrealdecls.(0) rctx
-  in
-  let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-  let ci = {
-    ci_ind = ind;
-    ci_npar = mib.mind_nparams;
-    ci_cstr_ndecls = mip.mind_consnrealdecls;
-    ci_cstr_nargs = mip.mind_consnrealargs;
-    ci_relevance = Declareops.relevance_of_projection_repr mib p;
-    ci_pp_info;
-  }
-  in
-  let x = match mib.mind_record with
-    | NotRecord | FakeRecord -> assert false
-    | PrimRecord info ->
-      let x, _, _, _ = info.(snd ind) in
-      make_annot (Name x) mip.mind_relevance
-  in
-  let indty = mkApp (indu, Context.Rel.instance mkRel 0 paramslet) in
-  let rec fold arg j subst = function
-    | [] -> assert false
-    | LocalAssum (na,ty) :: rem ->
-      let ty = Vars.substl subst (liftn 1 j ty) in
-      if arg != proj_arg then
-        let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in
-        let proj_relevant = match na.binder_relevance with
-        | Sorts.Irrelevant -> false
-        | Sorts.Relevant -> true
-        | Sorts.RelevanceVar _ -> assert false
-        in
-        let kn = Projection.Repr.make ind ~proj_relevant ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
-        fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
-      else
-        let p = ([|x|], liftn 1 2 ty) in
-        let branch =
-          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
-          (nas, mkRel (List.length ctx - (j - 1)))
-        in
-        let params = Context.Rel.instance mkRel 1 paramslet in
-        let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
-        it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
-    | LocalDef (_,c,t) :: rem ->
-      let c = liftn 1 j c in
-      let c1 = Vars.substl subst c in
-      fold arg (j+1) (c1::subst) rem
-  in
-  fold 0 1 [] (List.rev ctx)
-
 let extract_constant env kn cb =
   let sg = Evd.from_env env in
   let r = GlobRef.ConstRef kn in
diff --git a/test-suite/bugs/bug_16288.v b/test-suite/bugs/bug_16288.v
new file mode 100644
index 0000000000000..83f8c50ddb226
--- /dev/null
+++ b/test-suite/bugs/bug_16288.v
@@ -0,0 +1,13 @@
+Module Type Nop. End Nop.
+Module Empty. End Empty.
+Module M (N : Nop).
+  Local Set Primitive Projections.
+  Record M_t_NonEmpty elt := { M_m :> list elt }.
+  Record M_t_NonEmpty' X Y := { a : X ; b : Y }.
+End M.
+Module M' := M Empty.
+Require Import Coq.extraction.Extraction.
+Require Import Coq.extraction.ExtrOcamlBasic.
+Extraction Language OCaml.
+Recursive Extraction M'.
+Extraction TestCompile M'.