From 6007579ade085a60664e6b0d4596ff98c51aabf9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Apr 2018 16:07:37 +0200 Subject: Using more general information for primitive records. This brings more compatibility with handling of mutual primitive records in the kernel. --- interp/declare.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'interp/declare.ml') diff --git a/interp/declare.ml b/interp/declare.ml index aa737239b..e79cc6079 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,11 +383,14 @@ 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,0) in + let spec,_ = Inductive.lookup_mind_specif env mind in match spec.mind_record with - | Some (Some (_, kns, _)) -> - let projs = Inductiveops.compute_projections env (mind, 0) in + | PrimRecord info -> + let _, kns, _ = info.(0) 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 @@ -410,8 +413,8 @@ let declare_projections univs mind = assert (Constant.equal kn kn') ) kns projs; true, true - | Some None -> true,false - | None -> false,false + | FakeRecord -> true,false + | NotRecord -> false,false (* for initial declaration *) let declare_mind mie = -- cgit v1.2.3