aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r--pretyping/coercion.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b062da1f4..6a7f90463 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -65,7 +65,7 @@ let apply_coercion_args env evd check isproj argl funj =
| h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
match kind_of_term (whd_all env evd (EConstr.of_constr typ)) with
| Prod (_,c1,c2) ->
- if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
+ if check && not (e_cumul env evdref (Retyping.get_type_of env evd (EConstr.of_constr h)) c1) then
raise NoCoercion;
apply_rec (h::acc) (subst1 h c2) restl
| _ -> anomaly (Pp.str "apply_coercion_args")
@@ -488,7 +488,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
let v2 = Option.map (fun v -> beta_applist evd' (EConstr.of_constr (lift 1 v),[EConstr.of_constr v1])) v in
let t2 = match v2 with
| None -> subst_term evd' (EConstr.of_constr v1) (EConstr.of_constr t2)
- | Some v2 -> Retyping.get_type_of env1 evd' v2 in
+ | Some v2 -> Retyping.get_type_of env1 evd' (EConstr.of_constr v2) in
let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
| _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))