diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-01-15 18:51:36 -0500 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-01-15 18:51:36 -0500 |
| commit | 082b9f2efb4a775caa2b49dafc1dfcfd09cf9948 (patch) | |
| tree | f5b50004ab480491d780510e97b0e426a0958712 /checker/inductive.ml | |
| parent | b2454de95c601785cb4a081fc2902cec14b9b266 (diff) | |
Christmas is over...
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index ad7c472d9..be0f220b2 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -281,9 +281,10 @@ let is_correct_arity env c (p,pj) ind specif params = (try conv env a1 a1' with NotConvertible -> raise (LocalArity None)); srec (push_rel (na1,None,a1) env) t ar' - | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) - let ksort = match (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s + | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) + let env' = push_rel (na1,None,a1) env in + let ksort = match (whd_betadeltaiota env' a2) with + | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in (try conv env a1 dep_ind |