in the expected types of application heads.
let expected_hetype =
(* Inefficient, the head is computed twice. But I know *)
(* of no other solution. *)
let expected_hetype =
(* Inefficient, the head is computed twice. But I know *)
(* of no other solution. *)
- R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
+ (head_beta_reduce
+ (R.whd context (CicTypeChecker.type_of_aux' metasenv context he)))
in
let hetype = type_of_aux context he (Some expected_hetype) in
let tlbody_and_type =
in
let hetype = type_of_aux context he (Some expected_hetype) in
let tlbody_and_type =