diff options
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index aa737239b..fcb62ac8c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -384,10 +384,12 @@ let inInductive : inductive_obj -> obj = let declare_projections univs mind = let env = Global.env () in - let spec,_ = Inductive.lookup_mind_specif env (mind,0) in - match spec.mind_record with - | Some (Some (_, kns, _)) -> - let projs = Inductiveops.compute_projections env (mind, 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 let univs = match univs with @@ -408,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 - | Some None -> true,false - | None -> 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 = |