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.
---
 kernel/nativecode.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9141686952..6821fc980c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1990,8 +1990,10 @@ let compile_mind prefix ~interactive mb mind stack =
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
     let projs = match mb.mind_record with
-    | None | Some None -> []
-    | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs
+    | NotRecord | FakeRecord -> []
+    | PrimRecord info ->
+      let _, _, pbs = info.(i) in
+      Array.fold_left_i add_proj [] pbs
     in
     projs @ constructors @ gtype :: accu :: stack
   in
-- 
cgit v1.2.3