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. --- kernel/environ.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d6c9117b..0e34a7165 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -515,11 +515,12 @@ let template_polymorphic_pind (ind,u) env = let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_projections = match mind.mind_record with - | None | Some None -> env.env_globals.env_projections - | Some (Some (id, kns, pbs)) -> - Array.fold_left2 (fun projs kn pb -> - Cmap_env.add kn pb projs) - env.env_globals.env_projections kns pbs + | NotRecord | FakeRecord -> env.env_globals.env_projections + | PrimRecord projs -> + Array.fold_left (fun accu (id, kns, pbs) -> + Array.fold_left2 (fun accu kn pb -> + Cmap_env.add kn pb accu) accu kns pbs) + env.env_globals.env_projections projs in let new_globals = { env.env_globals with -- cgit v1.2.3