From 8b2a58026afe06d28238c374c0136bf1be6750a6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 8 Jun 2018 09:07:01 +0200
Subject: Handle mutual records in upper layers.

---
 interp/declare.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index e79cc6079..fcb62ac8c 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -383,13 +383,12 @@ let inInductive : inductive_obj -> obj =
     rebuild_function = infer_inductive_subtyping }
 
 let declare_projections univs mind =
-  (** FIXME: handle mutual records *)
-  let mind = (mind, 0) in
   let env = Global.env () in
-  let spec,_ = Inductive.lookup_mind_specif env mind in
-    match spec.mind_record with
-    | PrimRecord info ->
-      let _, kns, _ = info.(0) in
+  let mib = Environ.lookup_mind mind env in
+  match mib.mind_record with
+  | PrimRecord info ->
+    let iter i (_, kns, _) =
+      let mind = (mind, i) in
       let projs = Inductiveops.compute_projections env mind in
       Array.iter2 (fun kn (term, types) ->
 	let id = Label.to_id (Constant.label kn) in
@@ -411,10 +410,12 @@ let declare_projections univs mind =
         let entry = definition_entry ~types ~univs term in
         let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
         assert (Constant.equal kn kn')
-      ) kns projs;
-      true, true
-    | FakeRecord -> true,false
-    | NotRecord -> false,false
+      ) kns projs
+    in
+    let () = Array.iteri iter info in
+    true, true
+  | FakeRecord -> true, false
+  | NotRecord -> false, false
 
 (* for initial declaration *)
 let declare_mind mie =
-- 
cgit v1.2.3