diff options
| author | Matthieu Sozeau | 2016-05-25 15:17:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-06 14:38:05 +0200 |
| commit | f8a5cb590352a617de38fdd8ba5ffff7691d9841 (patch) | |
| tree | 5a4414e9e6d41fe0ebcccf5b25770b20bc31469d /pretyping/cases.ml | |
| parent | f77c2b488ca552b2316d4ebab1c051cb5a1347ab (diff) | |
Disallow dependent case on prim records w/o eta
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 985ad4b0d3..447a4c487c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1329,14 +1329,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn *) -let mk_case pb (ci,pred,c,brs) = - let mib = lookup_mind (fst ci.ci_ind) pb.env in - match mib.mind_record with - | Some (Some (_, cs, pbs)) -> - Reduction.beta_appvect brs.(0) - (Array.map (fun p -> mkProj (Projection.make p true, c)) cs) - | _ -> mkCase (ci,pred,c,brs) - (**********************************************************************) (* Main compiling descent *) let rec compile pb = @@ -1383,7 +1375,9 @@ and match_current pb (initial,tomatch) = pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota !(pb.evdref) pred in - let case = mk_case pb (ci,pred,current,brvals) in + let case = + make_case_or_project pb.env indf ci pred current brvals + in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist typ inst } |