| (_,_,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:" ^
| (_,_,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
let (_,ty,_) = List.nth fl i in
ty,ugraph2
- and check_exp_named_subst ~logger ~subst context ugraph =
+ and check_exp_named_subst ~logger ~subst context =
let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
match l with
[] -> ugraph
raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
end
in
- check_exp_named_subst_aux ~logger [] ugraph
+ check_exp_named_subst_aux ~logger []
and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
let module C = Cic in