Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

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)