diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-17 16:07:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 01:38:33 +0200 |
| commit | 6007579ade085a60664e6b0d4596ff98c51aabf9 (patch) | |
| tree | 58c0b5ae6c6f77b31df07e0bd906f56c23ec044a /pretyping/inductiveops.ml | |
| parent | c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 (diff) | |
Using more general information for primitive records.
This brings more compatibility with handling of mutual primitive records
in the kernel.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1003f86c5..d599afe69 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == BiFinite - | _ -> true + | PrimRecord _ -> mib.mind_finite == BiFinite + | NotRecord | FakeRecord -> true (* Annotation for cases *) let make_case_info env ind style = @@ -346,8 +346,10 @@ let get_constructors env (ind,params) = let get_projections env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in match mib.mind_record with - | Some (Some (id, projs, pbs)) -> Some projs - | _ -> None + | PrimRecord infos -> + let (_, projs, _) = infos.(snd (fst ind)) in + Some projs + | NotRecord | FakeRecord -> None let make_case_or_project env sigma indf ci pred c branches = let open EConstr in @@ -460,7 +462,7 @@ let build_branch_type env sigma dep p cs = build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections env (kn, _ as ind) = +let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in let indu = match mib.mind_universes with @@ -470,9 +472,9 @@ let compute_projections env (kn, _ as ind) = mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) in let x = match mib.mind_record with - | None | Some None -> + | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") - | Some (Some (id, _, _)) -> Name id + | PrimRecord info-> Name (pi1 (info.(i))) in (** FIXME: handle mutual records *) let pkt = mib.mind_packets.(0) in |