diff options
| author | Pierre-Marie Pédrot | 2018-06-19 16:17:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-19 16:17:40 +0200 |
| commit | c37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (patch) | |
| tree | 873e3f19156ed947e539eddcf5405e64f15e0194 /pretyping/cases.ml | |
| parent | a5722cc823dcf13594098dd21813feaaaf893bf0 (diff) | |
| parent | bc103cc493b2127f8a570bcf2e8be94378d79a55 (diff) | |
Merge PR #6754: Better elaboration of pattern-matchings on primitive projections
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0dd3c5944c..93ca9dc5e5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1425,7 +1425,7 @@ and match_current pb (initial,tomatch) = let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = - make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals + make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; |