From c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Jun 2018 14:59:15 +0200
Subject: Change the proj_ind field from MutInd.t to inductive.

This is a first step towards the acceptance of mutual record types in the
kernel.
---
 plugins/extraction/extraction.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3a61c7747d..bbf56525a7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,8 +1069,7 @@ let extract_constant env kn cb =
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                (** FIXME: handle mutual records *)
-                let ind = (pb.Declarations.proj_ind, 0) in
+                let ind = pb.Declarations.proj_ind in
                 let bodies = Inductiveops.legacy_match_projection env ind in
                 let body = bodies.(pb.Declarations.proj_arg) in
                 mk_typ (EConstr.of_constr body))
@@ -1086,8 +1085,7 @@ let extract_constant env kn cb =
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                (** FIXME: handle mutual records *)
-                let ind = (pb.Declarations.proj_ind, 0) in
+                let ind = pb.Declarations.proj_ind in
                 let bodies = Inductiveops.legacy_match_projection env ind in
                 let body = bodies.(pb.Declarations.proj_arg) in
                 mk_def (EConstr.of_constr body))
-- 
cgit v1.2.3


From 6007579ade085a60664e6b0d4596ff98c51aabf9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Apr 2018 16:07:37 +0200
Subject: Using more general information for primitive records.

This brings more compatibility with handling of mutual primitive records
in the kernel.
---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index bbf56525a7..71e09992cc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -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
-- 
cgit v1.2.3