From 1af95525a2a791889e6d72dfc150ff8f09a21e21 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 20:13:28 +0200
Subject: Fixing a bug in the presence of let-in while inferring the return
 clause.

---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 447a4c487c..fe2b0a5a1a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1871,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
-  let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
+  let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
   let subst, len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
-- 
cgit v1.2.3