aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-28 10:54:52 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-28 10:54:52 +0200
commit809eaea3c179ca23036ae807e8f8c1a749a027f7 (patch)
tree86a7f7a0484eee820dc0d7f57d3707e902210da6 /interp
parent2a036e512024d522846cc1b900ad06fe71c5733a (diff)
parent1e3d00fa7ef1641a1439be815ea5aa2624b7e728 (diff)
Merge PR #7866: Implementation of mutual records in the higher strata
Diffstat (limited to 'interp')
-rw-r--r--interp/declare.ml21
1 files changed, 11 insertions, 10 deletions
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 =