diff options
Diffstat (limited to 'interp/declare.ml')
-rw-r--r-- | interp/declare.ml | 21 |
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 = |