diff options
| author | Hugo Herbelin | 2015-12-15 14:35:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-15 15:27:57 +0100 |
| commit | 087c61eb7fcf17d4ef6ac5b40765e567b9cbcdc8 (patch) | |
| tree | e2c311fa87a0a8a6e62978c5e22e91a09f207db5 | |
| parent | a4a0a47dce78a7d580e172331e7e1ee2881dc689 (diff) | |
Fixing unexpected length of context in a typing function, detected by
cleaning done in e8c47b652a0.
It had no serious consequences except having whd-reduction blocked on
a let-in when typing a return clause with let-ins in the arity (a
priori resulting in return types of the form e.g. "(let x:=t in fun y
=> T) u" instead of T[x:=t;y:=u], if I'm not mistaking).
This fixes 3210.v in test-suite.
| -rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 15abfefb15..2f9803b62f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -111,7 +111,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let p = pj.uj_val in let univ = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in - let n = (snd specif).Declarations.mind_nrealargs in + let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in (lc, ty, univ) |