diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 12:13:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 12:13:03 +0200 |
| commit | 3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c (patch) | |
| tree | c15478f2305b3055c36b4d08e1b94ba4341806a7 | |
| parent | 91274486fab8712cb6b1c338704884c102ab005a (diff) | |
Fix bug #3584, elaborating pattern-matching on primitive records to the
use of projections.
| -rw-r--r-- | pretyping/cases.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3584.v | 16 |
2 files changed, 24 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 560289d1e..f9bd2d405 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1277,6 +1277,13 @@ 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 (cs, pbs) when Array.length pbs > 0 -> + Reduction.beta_appvect brs.(0) (Array.map (fun p -> mkProj (p, c)) cs) + | _ -> mkCase (ci,pred,c,brs) + (**********************************************************************) (* Main compiling descent *) let rec compile pb = @@ -1323,7 +1330,7 @@ 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 = mkCase (ci,pred,current,brvals) in + let case = mk_case pb (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 } diff --git a/test-suite/bugs/closed/3584.v b/test-suite/bugs/closed/3584.v new file mode 100644 index 000000000..3d4660b48 --- /dev/null +++ b/test-suite/bugs/closed/3584.v @@ -0,0 +1,16 @@ +Set Primitive Projections. +Set Implicit Arguments. +Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. +Definition eta_sigma {A} {P : A -> Type} (u : sigT P) + : existT _ (projT1 u) (projT2 u) = u + := match u with existT _ x y => eq_refl end. (* Toplevel input, characters 0-139: +Error: Pattern-matching expression on an object of inductive type sigT +has invalid information. *) +Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B)) +: A + B + := match x with + | existT _ true a => inl a + | existT _ false b => inr b + end. (* Toplevel input, characters 0-182: +Error: Pattern-matching expression on an object of inductive type sigT +has invalid information. *)
\ No newline at end of file |