From 43104a0b94e42fb78764b5d1365ca1e85a158508 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 10 Sep 2016 11:31:01 +0200 Subject: Fixing #5077 (failure on typing a fixpoint with evars in its type). Typing.type_of was using conversion for types of fixpoints while it could have used unification. --- pretyping/typing.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'pretyping/typing.ml') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index eb16628b1..bb3f19859 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -126,6 +126,16 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_type_fixpoint loc env evdref lna lar vdefj = + let lt = Array.length vdefj in + if Int.equal (Array.length lar) lt then + for i = 0 to lt-1 do + if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref + i lna vdefj lar + done + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in @@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = type_fixpoint env1 names lara vdefj in + let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) -- cgit v1.2.3