| C.Lambda (n,s,t) ->
(* Let's visit all the subterms that will not be visited later *)
let _ = type_of_aux context s None in
- let expected_target_type =
+ let n, expected_target_type =
match expectedty with
- None -> None
+ | None -> n, None
| Some expectedty' ->
- let ty =
+ let n, ty =
match R.whd context expectedty' with
- C.Prod (_,_,expected_target_type) ->
- beta_reduce expected_target_type
+ | C.Prod (n',_,expected_target_type) ->
+ let xtt = beta_reduce expected_target_type in
+ if n <> C.Anonymous then n, xtt else n', xtt
| _ -> assert false
in
- Some ty
+ n, Some ty
in
let type2 =
type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type