From 087c61eb7fcf17d4ef6ac5b40765e567b9cbcdc8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Dec 2015 14:35:29 +0100
Subject: 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.
---
 pretyping/typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)
 
-- 
cgit v1.2.3