| (_,_,ty,_)::_ ->
fst (split_prods ~subst [] paramsno ty)
in
- (tys@lefts,List.length tl,isinductive,paramsno,cl')
+ (lefts@tys,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
| (_,_,ty,_)::_ ->
fst (split_prods ~subst [] paramsno ty)
in
- (tys@lefts,List.length tl,isinductive,paramsno,cl')
+ (lefts@tys,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
function
C.Rel m when m > n && m <= nn -> false
| C.Rel m ->
- (match List.nth context (n-1) with
+ (match List.nth context (m-1) with
Some (_,C.Decl _) -> true
| Some (_,C.Def (bo,_)) ->
- guarded_by_destructors ~subst context m nn kl x safes
+ guarded_by_destructors ~subst context n nn kl x safes
(CicSubstitution.lift m bo)
| None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
)
| (_,_,ty,_)::_ ->
fst (split_prods ~subst [] paramsno ty)
in
- (tys@lefts,len,isinductive,paramsno,cl')
+ (lefts@tys,len,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
| (_,_,ty,_)::_ ->
fst (split_prods ~subst [] paramsno ty)
in
- (tys@lefts,List.length tl,isinductive,paramsno,cl')
+ (lefts@tys,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
| C.LetIn (n,s,ty,t) ->
(* only to check if s is well-typed *)
let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+ let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
let b,ugraph1 =
R.are_convertible ~subst ~metasenv context ty ty' ugraph1
in