| C.Prod (name,s,t) ->
let sort1 = type_of_aux context s
and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
- sort_of_prod context (name,s) (sort1,sort2)
+ let res = sort_of_prod context (name,s) (sort1,sort2) in
+ res
| C.Lambda (n,s,t) ->
let sort1 = type_of_aux context s in
(match R.whd context sort1 with
(CicSubstitution.subst s
(type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he
- and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
+ let hetype = type_of_aux context he in
+ let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->