aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/subtac_cases.ml24
-rw-r--r--contrib/subtac/subtac_coercion.ml10
-rw-r--r--contrib/subtac/subtac_command.ml4
-rw-r--r--contrib/subtac/subtac_obligations.ml2
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml6
5 files changed, 23 insertions, 23 deletions
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index e54c59058f..34c398289a 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -385,7 +385,7 @@ let mkDeclTomatch na = function
let map_tomatch_type f = function
| IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
- | NotInd (c,t) -> NotInd (option_map f c, f t)
+ | NotInd (c,t) -> NotInd (Option.map f c, f t)
let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -1127,7 +1127,7 @@ let rec generalize_problem pb = function
let tomatch = regeneralize_index_tomatch (i+1) tomatch in
{ pb with
tomatch = Abstract d :: tomatch;
- pred = option_map (generalize_predicate i d) pb'.pred }
+ pred = Option.map (generalize_predicate i d) pb'.pred }
(* No more patterns: typing the right-hand-side of equations *)
let build_leaf pb =
@@ -1142,7 +1142,7 @@ let build_leaf pb =
let shift_problem (current,t) pb =
{pb with
tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
- pred = option_map (specialize_predicate_var (current,t)) pb.pred;
+ pred = Option.map (specialize_predicate_var (current,t)) pb.pred;
history = push_history_pattern 0 AliasLeaf pb.history;
mat = List.map remove_current_pattern pb.mat }
@@ -1207,7 +1207,7 @@ let build_branch current deps pb eqns const_info =
let cur_alias = lift (List.length sign) current in
let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
let env' = push_rels sign pb.env in
- let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
+ let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
sign,
{ pb with
env = env';
@@ -1279,7 +1279,7 @@ and compile_generalization pb d rest =
{ pb with
env = push_rel d pb.env;
tomatch = rest;
- pred = option_map ungeneralize_predicate pb.pred;
+ pred = Option.map ungeneralize_predicate pb.pred;
mat = List.map (push_rels_eqn [d]) pb.mat } in
let j = compile pb in
{ uj_val = mkLambda_or_LetIn d j.uj_val;
@@ -1304,7 +1304,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
{pb with
env = newenv;
tomatch = tomatch;
- pred = option_map (lift_predicate n) pb.pred;
+ pred = Option.map (lift_predicate n) pb.pred;
history = history;
mat = mat } in
let j = compile pb in
@@ -1487,7 +1487,7 @@ let extract_arity_signature env0 tomatchl tmsign =
match tm with
| NotInd (bo,typ) ->
(match t with
- | None -> [na,option_map (lift n) bo,lift n typ]
+ | None -> [na,Option.map (lift n) bo,lift n typ]
| Some (loc,_,_,_) ->
user_err_loc (loc,"",
str "Unexpected type annotation for a term of non inductive type"))
@@ -1765,14 +1765,14 @@ let subst_rel_context k ctx subst =
let (_, ctx') =
List.fold_right
(fun (n, b, t) (k, acc) ->
- (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc))
+ (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
ctx (k, [])
in ctx'
let lift_rel_contextn n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
- (na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+ (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
| [] -> []
in
liftrec (rel_context_length sign + k) sign
@@ -2065,7 +2065,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
let liftn_rel_context n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
- (na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+ (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
| [] -> []
in
liftrec (k + rel_context_length sign) sign
@@ -2074,10 +2074,10 @@ let nf_evars_env evar_defs (env : env) : env =
let nf t = nf_isevar evar_defs t in
let env0 : env = reset_context env in
let f e (na, b, t) e' : env =
- Environ.push_named (na, option_map nf b, nf t) e'
+ Environ.push_named (na, Option.map nf b, nf t) e'
in
let env' = Environ.fold_named_context f ~init:env0 env in
- Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e')
+ Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
~init:env' env
let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 1fb079fac6..17bbb65bdc 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))
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index d7d304279a..49eab5d29d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -159,7 +159,7 @@ let list_of_local_binders l =
let lift_binders k n l =
let rec aux n = function
- | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+ | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
| [] -> []
in aux n l
@@ -326,7 +326,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
- (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
+ (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
let build_mutrec lnameargsardef boxed =
let sigma = Evd.empty and env = Global.env () in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 769aff9dcf..5e7f025be1 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -58,7 +58,7 @@ let subst_deps obls deps t =
let xobl = obls.(x) in
debug 3 (str "Trying to get body of obligation " ++ int x);
let oblb =
- try out_some xobl.obl_body
+ try Option.get xobl.obl_body
with _ ->
debug 3 (str "Couldn't get body of obligation " ++ int x);
assert(false)
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index ab542feb20..0ed0632c65 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -290,7 +290,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
let typ' = nf_isevar !isevars typ in
let tycon =
- option_map
+ Option.map
(fun (abs, ty) ->
match abs with
None ->
@@ -306,7 +306,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
apply_rec env (n+1)
{ uj_val = nf_isevar !isevars value;
uj_type = nf_isevar !isevars typ' }
- (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
+ (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
| _ ->
let hj = pretype empty_tycon env isevars lvar c in
@@ -314,7 +314,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(join_loc floc argloc) env (evars_of !isevars)
resj [hj]
in
- let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
+ let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
let resj =
match kind_of_term resj.uj_val with
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-13 17:43:21 +0000