diff options
| -rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6486435ca2..2157c4ef6a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1274,12 +1274,14 @@ let applyHead env evd n c = else match EConstr.kind evd (whd_all env evd cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + let (evd,evar) = + Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 + in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd | _ -> user_err Pp.(str "Apply_Head_Then") in - apprec n c (Typing.unsafe_type_of env evd c) evd + let evd, t = Typing.type_of env evd c in + apprec n c t evd let is_mimick_head sigma ts f = match EConstr.kind sigma f with |