From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 interp/discharge.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'interp/discharge.ml')

diff --git a/interp/discharge.ml b/interp/discharge.ml
index e16a955d..0e44a8b4 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -111,9 +111,10 @@ let process_inductive info modlist mib =
   let section_decls' = Context.Named.map discharge section_decls in
   let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
   let record = match mib.mind_record with
-    | Some (Some (id, _, _)) -> Some (Some id)
-    | Some None -> Some None
-    | None -> None
+    | PrimRecord info ->
+      Some (Some (Array.map pi1 info))
+    | FakeRecord -> Some None
+    | NotRecord -> None
   in
   { mind_entry_record = record;
     mind_entry_finite = mib.mind_finite;
-- 
cgit v1.2.3