diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-18 14:11:39 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-18 14:11:39 +0000 |
| commit | a7d06e11179d5d96a98382add560ed399b96712b (patch) | |
| tree | bf4cc50c6f2329cbbce45b7f3b5dbfe4f44681f2 /kernel | |
| parent | 1f7d439e1ca5c78623b9884fa987f09e606436e8 (diff) | |
bug fix: term reduced in bad env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4407 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 13dd9c550..56f6cb8a1 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -167,15 +167,15 @@ let is_correct_arity env c pj ind mip params = let kelim = mip.mind_kelim in let arsign,s = get_arity mip params in let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in - let rec srec pt t u = + let rec srec env pt t u = let pt' = whd_betadeltaiota env pt in let t' = whd_betadeltaiota env t in match kind_of_term pt', kind_of_term t' with - | Prod (_,a1,a2), Prod (_,a1',a2') -> + | Prod (na1,a1,a2), Prod (_,a1',a2') -> let univ = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec a2 a2' (Constraint.union u univ) + srec (push_rel (na1,None,a1) env) a2 a2' (Constraint.union u univ) | Prod (_,a1,a2), _ -> let k = whd_betadeltaiota env a2 in let ksort = match kind_of_term k with @@ -200,7 +200,7 @@ let is_correct_arity env c pj ind mip params = else raise (LocalArity (Some(pt',t',error_elim_expln env pt' t'))) in - try srec pj.uj_type nodep_ar Constraint.empty + try srec env pj.uj_type nodep_ar Constraint.empty with LocalArity kinds -> let create_sort = function | InProp -> mkProp |