diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 62e29dc06..f3468bcbf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -184,7 +184,7 @@ module Default = struct kind_of_term (whd_betadeltaiota env (evars_of evd) c1) with | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_map (whd_betadeltaiota env (evars_of evd)) v in + let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in let (evd',b) = match v' with | Some v' -> @@ -201,7 +201,7 @@ module Default = struct let env1 = push_rel (x,None,v1) env in let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' (Some v2) t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', + (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', mkProd (x, v1, t2')) | None -> (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) @@ -219,7 +219,7 @@ module Default = struct let (evd'', v2', t2') = let v2 = match v with - | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1' + | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1' | None -> None and evd', t2 = match v1' with @@ -231,7 +231,7 @@ module Default = struct in inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2', mkProd (name, u1, t2'))) | _ -> raise NoCoercion |