diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 20:13:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 20:14:45 +0200 |
| commit | 1af95525a2a791889e6d72dfc150ff8f09a21e21 (patch) | |
| tree | 61d50cf1d1164a598f80acb65d95b291ecbbbd81 /pretyping/cases.ml | |
| parent | 219f38188f71bfc665428f2a0f230001cada1e23 (diff) | |
Fixing a bug in the presence of let-in while inferring the return clause.
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 447a4c487..fe2b0a5a1 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 |