diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 1fb079fac..17bbb65bd 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -305,7 +305,7 @@ module Coercion = struct let coerce_itf loc env isevars v t c1 = let evars = ref isevars in let coercion = coerce loc env evars t c1 in - !evars, option_map (app_opt coercion) v, t + !evars, Option.map (app_opt coercion) v, t (* Taken from pretyping/coercion.ml *) @@ -439,7 +439,7 @@ module Coercion = struct (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in + let v' = Option.map (whd_betadeltaiota env (evars_of isevars)) v in let (evd',b) = match v' with Some v' -> @@ -455,7 +455,7 @@ module Coercion = 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 *) @@ -472,7 +472,7 @@ module Coercion = struct let (evd'', v2', t2') = let v2 = match v with - Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' + Some v -> Option.map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' | None -> None and evd', t2 = match v1' with @@ -483,7 +483,7 @@ module Coercion = 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)) |